author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14941 | 1edb674e0c33 |
child 15013 | 34264f5e4691 |
permissions | -rw-r--r-- |
13876 | 1 |
(* Title: HOL/Integ/presburger.ML |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb and Stefan Berghofer, TU Muenchen |
|
4 |
||
5 |
Tactic for solving arithmetical Goals in Presburger Arithmetic |
|
6 |
*) |
|
7 |
||
14811
9144ec118703
abstraction over functions is no default any more.
chaieb
parents:
14801
diff
changeset
|
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 |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
9 |
*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
10 |
|
13876 | 11 |
signature PRESBURGER = |
12 |
sig |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
13 |
val presburger_tac : bool -> bool -> int -> tactic |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
14 |
val presburger_method : bool -> bool -> int -> Proof.method |
13876 | 15 |
val setup : (theory -> theory) list |
16 |
val trace : bool ref |
|
17 |
end; |
|
18 |
||
19 |
structure Presburger: PRESBURGER = |
|
20 |
struct |
|
21 |
||
22 |
val trace = ref false; |
|
23 |
fun trace_msg s = if !trace then tracing s else (); |
|
24 |
||
25 |
(*-----------------------------------------------------------------*) |
|
26 |
(*cooper_pp: provefunction for the one-exstance quantifier elimination*) |
|
27 |
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*) |
|
28 |
(*-----------------------------------------------------------------*) |
|
29 |
||
14941 | 30 |
|
31 |
(* Invoking the oracle *) |
|
32 |
||
33 |
fun pres_oracle sg t = |
|
34 |
invoke_oracle (the_context()) "presburger_oracle" |
|
35 |
(sg, CooperDec.COOPER_ORACLE t) ; |
|
36 |
||
14801
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
37 |
val presburger_ss = simpset_of (theory "Presburger"); |
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
38 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
39 |
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |
13876 | 40 |
let val (xn1,p1) = variant_abs (xn,xT,p) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
41 |
in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end; |
13876 | 42 |
|
43 |
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm |
|
44 |
(CooperProof.proof_of_evalc sg); |
|
45 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
46 |
fun tmproof_of_int_qelim sg fm = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
47 |
Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel |
13876 | 48 |
(CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm; |
49 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
50 |
|
13876 | 51 |
(* Theorems to be used in this tactic*) |
52 |
||
53 |
val zdvd_int = thm "zdvd_int"; |
|
54 |
val zdiff_int_split = thm "zdiff_int_split"; |
|
55 |
val all_nat = thm "all_nat"; |
|
56 |
val ex_nat = thm "ex_nat"; |
|
57 |
val number_of1 = thm "number_of1"; |
|
58 |
val number_of2 = thm "number_of2"; |
|
59 |
val split_zdiv = thm "split_zdiv"; |
|
60 |
val split_zmod = thm "split_zmod"; |
|
61 |
val mod_div_equality' = thm "mod_div_equality'"; |
|
62 |
val split_div' = thm "split_div'"; |
|
63 |
val Suc_plus1 = thm "Suc_plus1"; |
|
64 |
val imp_le_cong = thm "imp_le_cong"; |
|
65 |
val conj_le_cong = thm "conj_le_cong"; |
|
66 |
||
67 |
(* extract all the constants in a term*) |
|
68 |
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs |
|
69 |
| add_term_typed_consts (t $ u, cs) = |
|
70 |
add_term_typed_consts (t, add_term_typed_consts (u, cs)) |
|
71 |
| add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs) |
|
72 |
| add_term_typed_consts (_, cs) = cs; |
|
73 |
||
74 |
fun term_typed_consts t = add_term_typed_consts(t,[]); |
|
75 |
||
76 |
(* Some Types*) |
|
77 |
val bT = HOLogic.boolT; |
|
78 |
val iT = HOLogic.intT; |
|
79 |
val binT = HOLogic.binT; |
|
80 |
val nT = HOLogic.natT; |
|
81 |
||
82 |
(* Allowed Consts in formulae for presburger tactic*) |
|
83 |
||
84 |
val allowed_consts = |
|
85 |
[("All", (iT --> bT) --> bT), |
|
86 |
("Ex", (iT --> bT) --> bT), |
|
87 |
("All", (nT --> bT) --> bT), |
|
88 |
("Ex", (nT --> bT) --> bT), |
|
89 |
||
90 |
("op &", bT --> bT --> bT), |
|
91 |
("op |", bT --> bT --> bT), |
|
92 |
("op -->", bT --> bT --> bT), |
|
93 |
("op =", bT --> bT --> bT), |
|
94 |
("Not", bT --> bT), |
|
95 |
||
96 |
("op <=", iT --> iT --> bT), |
|
97 |
("op =", iT --> iT --> bT), |
|
98 |
("op <", iT --> iT --> bT), |
|
99 |
("Divides.op dvd", iT --> iT --> bT), |
|
100 |
("Divides.op div", iT --> iT --> iT), |
|
101 |
("Divides.op mod", iT --> iT --> iT), |
|
102 |
("op +", iT --> iT --> iT), |
|
103 |
("op -", iT --> iT --> iT), |
|
104 |
("op *", iT --> iT --> iT), |
|
105 |
("HOL.abs", iT --> iT), |
|
106 |
("uminus", iT --> iT), |
|
14801
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
107 |
("HOL.max", iT --> iT --> iT), |
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
108 |
("HOL.min", iT --> iT --> iT), |
13876 | 109 |
|
110 |
("op <=", nT --> nT --> bT), |
|
111 |
("op =", nT --> nT --> bT), |
|
112 |
("op <", nT --> nT --> bT), |
|
113 |
("Divides.op dvd", nT --> nT --> bT), |
|
114 |
("Divides.op div", nT --> nT --> nT), |
|
115 |
("Divides.op mod", nT --> nT --> nT), |
|
116 |
("op +", nT --> nT --> nT), |
|
117 |
("op -", nT --> nT --> nT), |
|
118 |
("op *", nT --> nT --> nT), |
|
119 |
("Suc", nT --> nT), |
|
14801
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
120 |
("HOL.max", nT --> nT --> nT), |
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
121 |
("HOL.min", nT --> nT --> nT), |
13876 | 122 |
|
123 |
("Numeral.bin.Bit", binT --> bT --> binT), |
|
124 |
("Numeral.bin.Pls", binT), |
|
125 |
("Numeral.bin.Min", binT), |
|
126 |
("Numeral.number_of", binT --> iT), |
|
127 |
("Numeral.number_of", binT --> nT), |
|
128 |
("0", nT), |
|
129 |
("0", iT), |
|
130 |
("1", nT), |
|
131 |
("1", iT), |
|
132 |
("False", bT), |
|
133 |
("True", bT)]; |
|
134 |
||
135 |
(* Preparation of the formula to be sent to the Integer quantifier *) |
|
136 |
(* elimination procedure *) |
|
137 |
(* Transforms meta implications and meta quantifiers to object *) |
|
138 |
(* implications and object quantifiers *) |
|
139 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
140 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
141 |
(*==================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
142 |
(* Abstracting on subterms ========*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
143 |
(*==================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
144 |
(* Returns occurences of terms that are function application of type int or nat*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
145 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
146 |
fun getfuncs fm = case strip_comb fm of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
147 |
(Free (_, T), ts as _ :: _) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
148 |
if body_type T mem [iT, nT] |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
149 |
andalso not (ts = []) andalso forall (null o loose_bnos) ts |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
150 |
then [fm] |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
151 |
else foldl op union ([], map getfuncs ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
152 |
| (Var (_, T), ts as _ :: _) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
153 |
if body_type T mem [iT, nT] |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
154 |
andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm] |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
155 |
else foldl op union ([], map getfuncs ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
156 |
| (Const (s, T), ts) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
157 |
if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT]) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
158 |
then foldl op union ([], map getfuncs ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
159 |
else [fm] |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
160 |
| (Abs (s, T, t), _) => getfuncs t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
161 |
| _ => []; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
162 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
163 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
164 |
fun abstract_pres sg fm = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
165 |
foldr (fn (t, u) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
166 |
let val T = fastype_of t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
167 |
in all T $ Abs ("x", T, abstract_over (t, u)) end) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
168 |
(getfuncs fm, fm); |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
169 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
170 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
171 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
172 |
(* hasfuncs_on_bounds dont care of the type of the functions applied! |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
173 |
It returns true if there is a subterm coresponding to the application of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
174 |
a function on a bounded variable. |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
175 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
176 |
Function applications are allowed only for well predefined functions a |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
177 |
consts*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
178 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
179 |
fun has_free_funcs fm = case strip_comb fm of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
180 |
(Free (_, T), ts as _ :: _) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
181 |
if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT])) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
182 |
then true |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
183 |
else exists (fn x => x) (map has_free_funcs ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
184 |
| (Var (_, T), ts as _ :: _) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
185 |
if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT]) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
186 |
then true |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
187 |
else exists (fn x => x) (map has_free_funcs ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
188 |
| (Const (s, T), ts) => exists (fn x => x) (map has_free_funcs ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
189 |
| (Abs (s, T, t), _) => has_free_funcs t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
190 |
|_ => false; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
191 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
192 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
193 |
(*returns true if the formula is relevant for presburger arithmetic tactic |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
194 |
The constants occuring in term t should be a subset of the allowed_consts |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
195 |
There also should be no occurences of application of functions on bounded |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
196 |
variables. Whenever this function will be used, it will be ensured that t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
197 |
will not contain subterms with function symbols that could have been |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
198 |
abstracted over.*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
199 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
200 |
fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
201 |
map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @ |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
202 |
map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
203 |
subset [iT, nT] |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
204 |
andalso not (has_free_funcs t); |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
205 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
206 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
207 |
fun prepare_for_presburger sg q fm = |
13876 | 208 |
let |
209 |
val ps = Logic.strip_params fm |
|
210 |
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
|
211 |
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
212 |
val _ = if relevant (rev ps) c then () |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
213 |
else (trace_msg ("Conclusion is not a presburger term:\n" ^ |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
214 |
Sign.string_of_term sg c); raise CooperDec.COOPER) |
13876 | 215 |
fun mk_all ((s, T), (P,n)) = |
216 |
if 0 mem loose_bnos P then |
|
217 |
(HOLogic.all_const T $ Abs (s, T, P), n) |
|
218 |
else (incr_boundvars ~1 P, n-1) |
|
219 |
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
|
14130 | 220 |
val (rhs,irhs) = partition (relevant (rev ps)) hs |
13876 | 221 |
val np = length ps |
222 |
val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) |
|
223 |
(ps,(foldr HOLogic.mk_imp (rhs, c), np)) |
|
224 |
val (vs, _) = partition (fn t => q orelse (type_of t) = nT) |
|
225 |
(term_frees fm' @ term_vars fm'); |
|
226 |
val fm2 = foldr mk_all2 (vs, fm') |
|
227 |
in (fm2, np + length vs, length rhs) end; |
|
228 |
||
229 |
(*Object quantifier to meta --*) |
|
230 |
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ; |
|
231 |
||
232 |
(* object implication to meta---*) |
|
233 |
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; |
|
234 |
||
235 |
(* the presburger tactic*) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
236 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
237 |
(* Parameters : q = flag for quantify ofer free variables ; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
238 |
a = flag for abstracting over function occurences |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
239 |
i = subgoal *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
240 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
241 |
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st => |
13876 | 242 |
let |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
243 |
val g = BasisLibrary.List.nth (prems_of st, i - 1) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
244 |
val sg = sign_of_thm st |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
245 |
(* The Abstraction step *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
246 |
val g' = if a then abstract_pres sg g else g |
13876 | 247 |
(* Transform the term*) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
248 |
val (t,np,nh) = prepare_for_presburger sg q g' |
13876 | 249 |
(* Some simpsets for dealing with mod div abs and nat*) |
250 |
val simpset0 = HOL_basic_ss |
|
251 |
addsimps [mod_div_equality', Suc_plus1] |
|
13997 | 252 |
addsplits [split_zdiv, split_zmod, split_div', split_min, split_max] |
13876 | 253 |
(* Simp rules for changing (n::int) to int n *) |
254 |
val simpset1 = HOL_basic_ss |
|
255 |
addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) |
|
256 |
[int_int_eq, zle_int, zless_int, zadd_int, zmult_int] |
|
257 |
addsplits [zdiff_int_split] |
|
258 |
(*simp rules for elimination of int n*) |
|
259 |
||
260 |
val simpset2 = HOL_basic_ss |
|
261 |
addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1] |
|
262 |
addcongs [conj_le_cong, imp_le_cong] |
|
263 |
(* simp rules for elimination of abs *) |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14130
diff
changeset
|
264 |
val simpset3 = HOL_basic_ss addsplits [abs_split] |
13876 | 265 |
val ct = cterm_of sg (HOLogic.mk_Trueprop t) |
266 |
(* Theorem for the nat --> int transformation *) |
|
267 |
val pre_thm = Seq.hd (EVERY |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
268 |
[simp_tac simpset0 1, |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
269 |
TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |
14801
2d27b5ebc447
- deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset
|
270 |
TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)] |
13876 | 271 |
(trivial ct)) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
272 |
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
13876 | 273 |
(* The result of the quantifier elimination *) |
274 |
val (th, tac) = case (prop_of pre_thm) of |
|
275 |
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
|
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
276 |
let val pth = |
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
277 |
(* If quick_and_dirty then run without proof generation as oracle*) |
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
278 |
if !quick_and_dirty |
14941 | 279 |
then pres_oracle sg (Pattern.eta_long [] t1) |
280 |
(* |
|
281 |
assume (cterm_of sg |
|
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
282 |
(HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) |
14941 | 283 |
*) |
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
284 |
else tmproof_of_int_qelim sg (Pattern.eta_long [] t1) |
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
285 |
in |
13876 | 286 |
(trace_msg ("calling procedure with term:\n" ^ |
287 |
Sign.string_of_term sg t1); |
|
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
288 |
((pth RS iffD2) RS pre_thm, |
13876 | 289 |
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
290 |
end |
13876 | 291 |
| _ => (pre_thm, assm_tac i) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
292 |
in (rtac (((mp_step nh) o (spec_step np)) th) i |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
293 |
THEN tac) st |
14130 | 294 |
end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st); |
13876 | 295 |
|
296 |
fun presburger_args meth = |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
297 |
let val parse_flag = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
298 |
Args.$$$ "no_quantify" >> K (apfst (K false)) |
14811
9144ec118703
abstraction over functions is no default any more.
chaieb
parents:
14801
diff
changeset
|
299 |
|| Args.$$$ "abs" >> K (apsnd (K true)); |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
300 |
in |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
301 |
Method.simple_args |
14882 | 302 |
(Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
14811
9144ec118703
abstraction over functions is no default any more.
chaieb
parents:
14801
diff
changeset
|
303 |
curry (foldl op |>) (true, false)) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
304 |
(fn (q,a) => fn _ => meth q a 1) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
305 |
end; |
13876 | 306 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
307 |
fun presburger_method q a i = Method.METHOD (fn facts => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
308 |
Method.insert_tac facts 1 THEN presburger_tac q a i) |
13876 | 309 |
|
310 |
val setup = |
|
311 |
[Method.add_method ("presburger", |
|
312 |
presburger_args presburger_method, |
|
313 |
"decision procedure for Presburger arithmetic"), |
|
314 |
ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} => |
|
315 |
{splits = splits, inj_consts = inj_consts, discrete = discrete, |
|
14811
9144ec118703
abstraction over functions is no default any more.
chaieb
parents:
14801
diff
changeset
|
316 |
presburger = Some (presburger_tac true false)})]; |
13876 | 317 |
|
318 |
end; |
|
319 |
||
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset
|
320 |
val presburger_tac = Presburger.presburger_tac true false; |