author | haftmann |
Tue, 05 Jun 2007 19:19:30 +0200 | |
changeset 23261 | 85f27f79232f |
parent 23197 | f96d909eda37 |
child 23297 | 06f108974fa1 |
permissions | -rw-r--r-- |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
1 |
(* Title: Provers/Arith/fast_lin_arith.ML |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1998 TU Munich |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
5 |
|
6062 | 6 |
A generic linear arithmetic package. |
6102 | 7 |
It provides two tactics |
8 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
9 |
lin_arith_tac: int -> tactic |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
10 |
cut_lin_arith_tac: thms -> int -> tactic |
6102 | 11 |
|
12 |
and a simplification procedure |
|
13 |
||
16458 | 14 |
lin_arith_prover: theory -> simpset -> term -> thm option |
6102 | 15 |
|
16 |
Only take premises and conclusions into account that are already (negated) |
|
17 |
(in)equations. lin_arith_prover tries to prove or disprove the term. |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
18 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
19 |
|
9073 | 20 |
(* Debugging: set Fast_Arith.trace *) |
7582 | 21 |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
22 |
(*** Data needed for setting up the linear arithmetic package ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
23 |
|
6102 | 24 |
signature LIN_ARITH_LOGIC = |
25 |
sig |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
26 |
val conjI : thm (* P ==> Q ==> P & Q *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
27 |
val ccontr : thm (* (~ P ==> False) ==> P *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
28 |
val notI : thm (* (P ==> False) ==> ~ P *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
29 |
val not_lessD : thm (* ~(m < n) ==> n <= m *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
30 |
val not_leD : thm (* ~(m <= n) ==> n < m *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
31 |
val sym : thm (* x = y ==> y = x *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
32 |
val mk_Eq : thm -> thm |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
33 |
val atomize : thm -> thm list |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
34 |
val mk_Trueprop : term -> term |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
35 |
val neg_prop : term -> term |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
36 |
val is_False : thm -> bool |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
37 |
val is_nat : typ list * term -> bool |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
38 |
val mk_nat_thm : theory -> term -> thm |
6102 | 39 |
end; |
40 |
(* |
|
41 |
mk_Eq(~in) = `in == False' |
|
42 |
mk_Eq(in) = `in == True' |
|
43 |
where `in' is an (in)equality. |
|
44 |
||
23190 | 45 |
neg_prop(t) = neg if t is wrapped up in Trueprop and neg is the |
46 |
(logically) negated version of t (again wrapped up in Trueprop), |
|
47 |
where the negation of a negative term is the term itself (no |
|
48 |
double negation!); raises TERM ("neg_prop", [t]) if t is not of |
|
49 |
the form 'Trueprop $ _' |
|
6128 | 50 |
|
51 |
is_nat(parameter-types,t) = t:nat |
|
52 |
mk_nat_thm(t) = "0 <= t" |
|
6102 | 53 |
*) |
54 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
55 |
signature LIN_ARITH_DATA = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
56 |
sig |
20268 | 57 |
(* internal representation of linear (in-)equations: *) |
58 |
type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
59 |
val decomp: theory -> term -> decompT option |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
60 |
val domain_is_nat : term -> bool |
20268 | 61 |
(* preprocessing, performed on a representation of subgoals as list of premises: *) |
62 |
val pre_decomp: theory -> typ list * term list -> (typ list * term list) list |
|
63 |
(* preprocessing, performed on the goal -- must do the same as 'pre_decomp': *) |
|
64 |
val pre_tac : int -> Tactical.tactic |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
65 |
val number_of : IntInf.int * typ -> term |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
66 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
67 |
(* |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
68 |
decomp(`x Rel y') should yield (p,i,Rel,q,j,d) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
69 |
where Rel is one of "<", "~<", "<=", "~<=" and "=" and |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
70 |
p (q, respectively) is the decomposition of the sum term x |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
71 |
(y, respectively) into a list of summand * multiplicity |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
72 |
pairs and a constant summand and d indicates if the domain |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
73 |
is discrete. |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
74 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
75 |
domain_is_nat(`x Rel y') t should yield true iff x is of type "nat". |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
76 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
77 |
The relationship between pre_decomp and pre_tac is somewhat tricky. The |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
78 |
internal representation of a subgoal and the corresponding theorem must |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
79 |
be modified by pre_decomp (pre_tac, resp.) in a corresponding way. See |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
80 |
the comment for split_items below. (This is even necessary for eta- and |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
81 |
beta-equivalent modifications, as some of the lin. arith. code is not |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
82 |
insensitive to them.) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
83 |
|
9420 | 84 |
ss must reduce contradictory <= to False. |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
85 |
It should also cancel common summands to keep <= reduced; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
86 |
otherwise <= can grow to massive proportions. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
87 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
88 |
|
6062 | 89 |
signature FAST_LIN_ARITH = |
90 |
sig |
|
15184 | 91 |
val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset
|
92 |
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} |
15184 | 93 |
-> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset
|
94 |
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) |
10575 | 95 |
-> theory -> theory |
19314 | 96 |
val trace: bool ref |
14510 | 97 |
val fast_arith_neq_limit: int ref |
16458 | 98 |
val lin_arith_prover: theory -> simpset -> term -> thm option |
17892 | 99 |
val lin_arith_tac: bool -> int -> tactic |
17613 | 100 |
val cut_lin_arith_tac: simpset -> int -> tactic |
6062 | 101 |
end; |
102 |
||
22846 | 103 |
functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC |
6102 | 104 |
and LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH = |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
105 |
struct |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
106 |
|
9420 | 107 |
|
108 |
(** theory data **) |
|
109 |
||
16458 | 110 |
structure Data = TheoryDataFun |
22846 | 111 |
( |
15184 | 112 |
type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset
|
113 |
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}; |
9420 | 114 |
|
10691 | 115 |
val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], |
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset
|
116 |
lessD = [], neqE = [], simpset = Simplifier.empty_ss}; |
9420 | 117 |
val copy = I; |
16458 | 118 |
val extend = I; |
9420 | 119 |
|
16458 | 120 |
fun merge _ |
121 |
({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, |
|
122 |
lessD = lessD1, neqE=neqE1, simpset = simpset1}, |
|
123 |
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, |
|
124 |
lessD = lessD2, neqE=neqE2, simpset = simpset2}) = |
|
9420 | 125 |
{add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), |
15184 | 126 |
mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2), |
10575 | 127 |
inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), |
128 |
lessD = Drule.merge_rules (lessD1, lessD2), |
|
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset
|
129 |
neqE = Drule.merge_rules (neqE1, neqE2), |
10575 | 130 |
simpset = Simplifier.merge_ss (simpset1, simpset2)}; |
22846 | 131 |
); |
9420 | 132 |
|
133 |
val map_data = Data.map; |
|
134 |
||
135 |
||
136 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
137 |
(*** A fast decision procedure ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
138 |
(*** Code ported from HOL Light ***) |
6056 | 139 |
(* possible optimizations: |
140 |
use (var,coeff) rep or vector rep tp save space; |
|
141 |
treat non-negative atoms separately rather than adding 0 <= atom |
|
142 |
*) |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
143 |
|
9073 | 144 |
val trace = ref false; |
145 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
146 |
datatype lineq_type = Eq | Le | Lt; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
147 |
|
6056 | 148 |
datatype injust = Asm of int |
149 |
| Nat of int (* index of atom *) |
|
6128 | 150 |
| LessD of injust |
151 |
| NotLessD of injust |
|
152 |
| NotLeD of injust |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
153 |
| NotLeDD of injust |
16358 | 154 |
| Multiplied of IntInf.int * injust |
155 |
| Multiplied2 of IntInf.int * injust |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
156 |
| Added of injust * injust; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
157 |
|
16358 | 158 |
datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
159 |
|
13498 | 160 |
(* ------------------------------------------------------------------------- *) |
161 |
(* Finding a (counter) example from the trace of a failed elimination *) |
|
162 |
(* ------------------------------------------------------------------------- *) |
|
163 |
(* Examples are represented as rational numbers, *) |
|
164 |
(* Dont blame John Harrison for this code - it is entirely mine. TN *) |
|
165 |
||
166 |
exception NoEx; |
|
167 |
||
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
168 |
(* Coding: (i,true,cs) means i <= cs and (i,false,cs) means i < cs. |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
169 |
In general, true means the bound is included, false means it is excluded. |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
170 |
Need to know if it is a lower or upper bound for unambiguous interpretation! |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
171 |
*) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
172 |
|
22950 | 173 |
fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)] |
174 |
| elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)] |
|
175 |
| elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)]; |
|
13498 | 176 |
|
177 |
(* PRE: ex[v] must be 0! *) |
|
22950 | 178 |
fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) = |
179 |
let |
|
180 |
val rs = map Rat.rat_of_int cs; |
|
181 |
val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero; |
|
23063 | 182 |
in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end; |
183 |
(* If nth rs v < 0, le should be negated. |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
184 |
Instead this swap is taken into account in ratrelmin2. |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
185 |
*) |
13498 | 186 |
|
22950 | 187 |
fun ratrelmin2 (x as (r, ler), y as (s, les)) = |
188 |
case Rat.cmp (r, s) |
|
189 |
of EQUAL => (r, (not ler) andalso (not les)) |
|
190 |
| LESS => x |
|
191 |
| GREATER => y; |
|
192 |
||
193 |
fun ratrelmax2 (x as (r, ler), y as (s, les)) = |
|
194 |
case Rat.cmp (r, s) |
|
195 |
of EQUAL => (r, ler andalso les) |
|
196 |
| LESS => y |
|
197 |
| GREATER => x; |
|
13498 | 198 |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
199 |
val ratrelmin = foldr1 ratrelmin2; |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
200 |
val ratrelmax = foldr1 ratrelmax2; |
13498 | 201 |
|
22950 | 202 |
fun ratexact up (r, exact) = |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
203 |
if exact then r else |
22950 | 204 |
let |
205 |
val (p, q) = Rat.quotient_of_rat r; |
|
206 |
val nth = Rat.inv (Rat.rat_of_int q); |
|
207 |
in Rat.add r (if up then nth else Rat.neg nth) end; |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
208 |
|
22950 | 209 |
fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two); |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
210 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
211 |
fun choose2 d ((lb, exactl), (ub, exactu)) = |
22950 | 212 |
let val ord = Rat.cmp_zero lb in |
213 |
if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu) |
|
214 |
then Rat.zero |
|
215 |
else if not d then |
|
216 |
if ord = GREATER |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
217 |
then if exactl then lb else ratmiddle (lb, ub) |
22950 | 218 |
else if exactu then ub else ratmiddle (lb, ub) |
219 |
else (*discrete domain, both bounds must be exact*) |
|
23025 | 220 |
if ord = GREATER |
22950 | 221 |
then let val lb' = Rat.roundup lb in |
222 |
if Rat.le lb' ub then lb' else raise NoEx end |
|
223 |
else let val ub' = Rat.rounddown ub in |
|
224 |
if Rat.le lb ub' then ub' else raise NoEx end |
|
225 |
end; |
|
13498 | 226 |
|
22950 | 227 |
fun findex1 discr (v, lineqs) ex = |
228 |
let |
|
23063 | 229 |
val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs; |
22950 | 230 |
val ineqs = maps elim_eqns nz; |
23063 | 231 |
val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs |
22950 | 232 |
val lb = ratrelmax (map (eval ex v) ge) |
233 |
val ub = ratrelmin (map (eval ex v) le) |
|
21109 | 234 |
in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end; |
13498 | 235 |
|
236 |
fun elim1 v x = |
|
23063 | 237 |
map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le, |
21109 | 238 |
nth_map v (K Rat.zero) bs)); |
13498 | 239 |
|
23063 | 240 |
fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs |
241 |
of [x] => x =/ nth cs v |
|
242 |
| _ => false; |
|
13498 | 243 |
|
244 |
(* The base case: |
|
245 |
all variables occur only with positive or only with negative coefficients *) |
|
246 |
fun pick_vars discr (ineqs,ex) = |
|
22950 | 247 |
let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.cmp_zero) cs) ineqs |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
248 |
in case nz of [] => ex |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
249 |
| (_,_,cs) :: _ => |
22950 | 250 |
let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs |
251 |
val d = nth discr v; |
|
23063 | 252 |
val pos = not (Rat.cmp_zero (nth cs v) = LESS); |
22950 | 253 |
val sv = filter (single_var v) nz; |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
254 |
val minmax = |
17951 | 255 |
if pos then if d then Rat.roundup o fst o ratrelmax |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
256 |
else ratexact true o ratrelmax |
17951 | 257 |
else if d then Rat.rounddown o fst o ratrelmin |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
258 |
else ratexact false o ratrelmin |
23063 | 259 |
val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (nth bs v)), le)) sv |
17951 | 260 |
val x = minmax((Rat.zero,if pos then true else false)::bnds) |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
261 |
val ineqs' = elim1 v x nz |
21109 | 262 |
val ex' = nth_map v (K x) ex |
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
263 |
in pick_vars discr (ineqs',ex') end |
13498 | 264 |
end; |
265 |
||
266 |
fun findex0 discr n lineqs = |
|
22950 | 267 |
let val ineqs = maps elim_eqns lineqs |
268 |
val rineqs = map (fn (a,le,cs) => (Rat.rat_of_int a, le, map Rat.rat_of_int cs)) |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
269 |
ineqs |
17951 | 270 |
in pick_vars discr (rineqs,replicate n Rat.zero) end; |
13498 | 271 |
|
272 |
(* ------------------------------------------------------------------------- *) |
|
23197 | 273 |
(* End of counterexample finder. The actual decision procedure starts here. *) |
13498 | 274 |
(* ------------------------------------------------------------------------- *) |
275 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
276 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
277 |
(* Calculate new (in)equality type after addition. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
278 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
279 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
280 |
fun find_add_type(Eq,x) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
281 |
| find_add_type(x,Eq) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
282 |
| find_add_type(_,Lt) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
283 |
| find_add_type(Lt,_) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
284 |
| find_add_type(Le,Le) = Le; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
285 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
286 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
287 |
(* Multiply out an (in)equation. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
288 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
289 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
290 |
fun multiply_ineq n (i as Lineq(k,ty,l,just)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
291 |
if n = 1 then i |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
292 |
else if n = 0 andalso ty = Lt then sys_error "multiply_ineq" |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
293 |
else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq" |
17524 | 294 |
else Lineq (n * k, ty, map (curry op* n) l, Multiplied (n, just)); |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
295 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
296 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
297 |
(* Add together (in)equations. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
298 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
299 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
300 |
fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = |
18330 | 301 |
let val l = map2 (curry (op +)) l1 l2 |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
302 |
in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
303 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
304 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
305 |
(* Elimination of variable between a single pair of (in)equations. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
306 |
(* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
307 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
308 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
309 |
fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = |
23063 | 310 |
let val c1 = nth l1 v and c2 = nth l2 v |
23261 | 311 |
val m = Integer.lcm (abs c1) (abs c2) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
312 |
val m1 = m div (abs c1) and m2 = m div (abs c2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
313 |
val (n1,n2) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
314 |
if (c1 >= 0) = (c2 >= 0) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
315 |
then if ty1 = Eq then (~m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
316 |
else if ty2 = Eq then (m1,~m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
317 |
else sys_error "elim_var" |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
318 |
else (m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
319 |
val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
320 |
then (~n1,~n2) else (n1,n2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
321 |
in add_ineq (multiply_ineq n1 i1) (multiply_ineq n2 i2) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
322 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
323 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
324 |
(* The main refutation-finding code. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
325 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
326 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
327 |
fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
328 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
329 |
fun is_answer (ans as Lineq(k,ty,l,_)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
330 |
case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
331 |
|
16358 | 332 |
fun calc_blowup (l:IntInf.int list) = |
17496 | 333 |
let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
334 |
in (length p) * (length n) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
335 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
336 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
337 |
(* Main elimination code: *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
338 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
339 |
(* (1) Looks for immediate solutions (false assertions with no variables). *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
340 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
341 |
(* (2) If there are any equations, picks a variable with the lowest absolute *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
342 |
(* coefficient in any of them, and uses it to eliminate. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
343 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
344 |
(* (3) Otherwise, chooses a variable in the inequality to minimize the *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
345 |
(* blowup (number of consequences generated) and eliminates it. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
346 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
347 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
348 |
fun allpairs f xs ys = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
349 |
List.concat (map (fn x => map (fn y => f x y) ys) xs); |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
350 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
351 |
fun extract_first p = |
15531 | 352 |
let fun extract xs (y::ys) = if p y then (SOME y,xs@ys) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
353 |
else extract (y::xs) ys |
15531 | 354 |
| extract xs [] = (NONE,xs) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
355 |
in extract [] end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
356 |
|
6056 | 357 |
fun print_ineqs ineqs = |
9073 | 358 |
if !trace then |
12262 | 359 |
tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => |
16358 | 360 |
IntInf.toString c ^ |
9073 | 361 |
(case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ |
16358 | 362 |
commas(map IntInf.toString l)) ineqs)) |
9073 | 363 |
else (); |
6056 | 364 |
|
13498 | 365 |
type history = (int * lineq list) list; |
366 |
datatype result = Success of injust | Failure of history; |
|
367 |
||
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
368 |
fun elim (ineqs, hist) = |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
369 |
let val dummy = print_ineqs ineqs |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
370 |
val (triv, nontriv) = List.partition is_trivial ineqs in |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
371 |
if not (null triv) |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
372 |
then case Library.find_first is_answer triv of |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
373 |
NONE => elim (nontriv, hist) |
15531 | 374 |
| SOME(Lineq(_,_,_,j)) => Success j |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
375 |
else |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
376 |
if null nontriv then Failure hist |
13498 | 377 |
else |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
378 |
let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
379 |
if not (null eqs) then |
15570 | 380 |
let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) |
16358 | 381 |
val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y))) |
15570 | 382 |
(List.filter (fn i => i<>0) clist) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
383 |
val c = hd sclist |
15531 | 384 |
val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) = |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
385 |
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
386 |
val v = find_index_eq c ceq |
23063 | 387 |
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
388 |
(othereqs @ noneqs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
389 |
val others = map (elim_var v eq) roth @ ioth |
13498 | 390 |
in elim(others,(v,nontriv)::hist) end |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
391 |
else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
392 |
let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs |
23063 | 393 |
val numlist = 0 upto (length (hd lists) - 1) |
394 |
val coeffs = map (fn i => map (fn xs => nth xs i) lists) numlist |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
395 |
val blows = map calc_blowup coeffs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
396 |
val iblows = blows ~~ numlist |
23063 | 397 |
val nziblows = filter_out (fn (i, _) => i = 0) iblows |
13498 | 398 |
in if null nziblows then Failure((~1,nontriv)::hist) |
399 |
else |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
400 |
let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) |
23063 | 401 |
val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs |
402 |
val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes |
|
13498 | 403 |
in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
404 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
405 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
406 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
407 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
408 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
409 |
(* Translate back a proof. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
410 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
411 |
|
20268 | 412 |
fun trace_thm (msg : string) (th : thm) : thm = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
413 |
(if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th); |
9073 | 414 |
|
20268 | 415 |
fun trace_msg (msg : string) : unit = |
12262 | 416 |
if !trace then tracing msg else (); |
9073 | 417 |
|
13498 | 418 |
(* FIXME OPTIMIZE!!!! (partly done already) |
6056 | 419 |
Addition/Multiplication need i*t representation rather than t+t+... |
10691 | 420 |
Get rid of Mulitplied(2). For Nat LA_Data.number_of should return Suc^n |
421 |
because Numerals are not known early enough. |
|
6056 | 422 |
|
423 |
Simplification may detect a contradiction 'prematurely' due to type |
|
424 |
information: n+1 <= 0 is simplified to False and does not need to be crossed |
|
425 |
with 0 <= n. |
|
426 |
*) |
|
427 |
local |
|
428 |
exception FalseE of thm |
|
429 |
in |
|
22846 | 430 |
fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm = |
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset
|
431 |
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = |
16458 | 432 |
Data.get sg; |
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
17613
diff
changeset
|
433 |
val simpset' = Simplifier.inherit_context ss simpset; |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
434 |
val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) => |
6056 | 435 |
map fst lhs union (map fst rhs union ats)) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
436 |
([], List.mapPartial (fn thm => if Thm.no_prems thm |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
437 |
then LA_Data.decomp sg (concl_of thm) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
438 |
else NONE) asms) |
6056 | 439 |
|
10575 | 440 |
fun add2 thm1 thm2 = |
6102 | 441 |
let val conj = thm1 RS (thm2 RS LA_Logic.conjI) |
15531 | 442 |
in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
443 |
end; |
15531 | 444 |
fun try_add [] _ = NONE |
10575 | 445 |
| try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of |
15531 | 446 |
NONE => try_add thm1s thm2 | some => some; |
10575 | 447 |
|
448 |
fun addthms thm1 thm2 = |
|
449 |
case add2 thm1 thm2 of |
|
15531 | 450 |
NONE => (case try_add ([thm1] RL inj_thms) thm2 of |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
451 |
NONE => ( the (try_add ([thm2] RL inj_thms) thm1) |
15660 | 452 |
handle Option => |
14360 | 453 |
(trace_thm "" thm1; trace_thm "" thm2; |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
454 |
sys_error "Lin.arith. failed to add thms") |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
455 |
) |
15531 | 456 |
| SOME thm => thm) |
457 |
| SOME thm => thm; |
|
10575 | 458 |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
459 |
fun multn(n,thm) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
460 |
let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th) |
6102 | 461 |
in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
462 |
|
15184 | 463 |
fun multn2(n,thm) = |
15531 | 464 |
let val SOME(mth) = |
465 |
get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms |
|
22596 | 466 |
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var; |
15184 | 467 |
val cv = cvar(mth, hd(prems_of mth)); |
468 |
val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv))) |
|
469 |
in instantiate ([],[(cv,ct)]) mth end |
|
10691 | 470 |
|
6056 | 471 |
fun simp thm = |
17515 | 472 |
let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) |
6102 | 473 |
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end |
6056 | 474 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
475 |
fun mk (Asm i) = trace_thm ("Asm " ^ Int.toString i) (nth asms i) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
476 |
| mk (Nat i) = trace_thm ("Nat " ^ Int.toString i) (LA_Logic.mk_nat_thm sg (nth atoms i)) |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
477 |
| mk (LessD j) = trace_thm "L" (hd ([mk j] RL lessD)) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
478 |
| mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
479 |
| mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
480 |
| mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
481 |
| mk (Added (j1, j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
482 |
| mk (Multiplied (n, j)) = (trace_msg ("*" ^ IntInf.toString n); trace_thm "*" (multn (n, mk j))) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
483 |
| mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ IntInf.toString n); trace_thm "**" (multn2 (n, mk j))) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
484 |
|
9073 | 485 |
in trace_msg "mkthm"; |
12932 | 486 |
let val thm = trace_thm "Final thm:" (mk just) |
17515 | 487 |
in let val fls = simplify simpset' thm |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
488 |
in trace_thm "After simplification:" fls; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
489 |
if LA_Logic.is_False fls then fls |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
490 |
else |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
491 |
(tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms; |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
492 |
tracing "Proved:"; tracing (Display.string_of_thm fls); |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
493 |
warning "Linear arithmetic should have refuted the assumptions.\n\ |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
494 |
\Please inform Tobias Nipkow (nipkow@in.tum.de)."; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
495 |
fls) |
12932 | 496 |
end |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
497 |
end handle FalseE thm => trace_thm "False reached early:" thm |
12932 | 498 |
end |
6056 | 499 |
end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
500 |
|
23261 | 501 |
fun coeff poly atom = |
502 |
AList.lookup (op =) poly atom |> the_default Integer.zero; |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
503 |
|
23261 | 504 |
fun lcms ks = fold Integer.lcm ks Integer.one; |
10691 | 505 |
|
506 |
fun integ(rlhs,r,rel,rrhs,s,d) = |
|
17951 | 507 |
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s |
508 |
val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs)) |
|
22846 | 509 |
fun mult(t,r) = |
17951 | 510 |
let val (i,j) = Rat.quotient_of_rat r |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15922
diff
changeset
|
511 |
in (t,i * (m div j)) end |
12932 | 512 |
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end |
10691 | 513 |
|
13498 | 514 |
fun mklineq n atoms = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
515 |
fn (item, k) => |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
516 |
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item |
13498 | 517 |
val lhsa = map (coeff lhs) atoms |
518 |
and rhsa = map (coeff rhs) atoms |
|
18330 | 519 |
val diff = map2 (curry (op -)) rhsa lhsa |
13498 | 520 |
val c = i-j |
521 |
val just = Asm k |
|
522 |
fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j)) |
|
523 |
in case rel of |
|
524 |
"<=" => lineq(c,Le,diff,just) |
|
525 |
| "~<=" => if discrete |
|
526 |
then lineq(1-c,Le,map (op ~) diff,NotLeDD(just)) |
|
527 |
else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) |
|
528 |
| "<" => if discrete |
|
529 |
then lineq(c+1,Le,diff,LessD(just)) |
|
530 |
else lineq(c,Lt,diff,just) |
|
531 |
| "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just)) |
|
532 |
| "=" => lineq(c,Eq,diff,just) |
|
22846 | 533 |
| _ => sys_error("mklineq" ^ rel) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
534 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
535 |
|
13498 | 536 |
(* ------------------------------------------------------------------------- *) |
537 |
(* Print (counter) example *) |
|
538 |
(* ------------------------------------------------------------------------- *) |
|
539 |
||
540 |
fun print_atom((a,d),r) = |
|
17951 | 541 |
let val (p,q) = Rat.quotient_of_rat r |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15922
diff
changeset
|
542 |
val s = if d then IntInf.toString p else |
13498 | 543 |
if p = 0 then "0" |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15922
diff
changeset
|
544 |
else IntInf.toString p ^ "/" ^ IntInf.toString q |
13498 | 545 |
in a ^ " = " ^ s end; |
546 |
||
19049 | 547 |
fun produce_ex sds = |
17496 | 548 |
curry (op ~~) sds |
549 |
#> map print_atom |
|
550 |
#> commas |
|
23197 | 551 |
#> curry (op ^) "Counterexample (possibly spurious):\n"; |
13498 | 552 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
553 |
fun trace_ex (sg, params, atoms, discr, n, hist : history) = |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
554 |
case hist of |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
555 |
[] => () |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
556 |
| (v, lineqs) :: hist' => |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
557 |
let val frees = map Free params |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
558 |
fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t)) |
22950 | 559 |
val start = if v = ~1 then (hist', findex0 discr n lineqs) |
560 |
else (hist, replicate n Rat.zero) |
|
561 |
val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) |
|
562 |
(uncurry (fold (findex1 discr)) start)) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
563 |
handle NoEx => NONE |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
564 |
in |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
565 |
case ex of |
23197 | 566 |
SOME s => (warning "arith failed - see trace for a counterexample"; tracing s) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
567 |
| NONE => warning "arith failed" |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
568 |
end; |
13498 | 569 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
570 |
(* ------------------------------------------------------------------------- *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
571 |
|
20268 | 572 |
fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
573 |
if LA_Logic.is_nat (pTs, atom) |
6056 | 574 |
then let val l = map (fn j => if j=i then 1 else 0) ixs |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
575 |
in SOME (Lineq (0, Le, l, Nat i)) end |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
576 |
else NONE; |
6056 | 577 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
578 |
(* This code is tricky. It takes a list of premises in the order they occur |
15531 | 579 |
in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical |
580 |
ones as NONE. Going through the premises, each numeric one is converted into |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
581 |
a Lineq. The tricky bit is to convert ~= which is split into two cases < and |
13498 | 582 |
>. Thus split_items returns a list of equation systems. This may blow up if |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
583 |
there are many ~=, but in practice it does not seem to happen. The really |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
584 |
tricky bit is to arrange the order of the cases such that they coincide with |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
585 |
the order in which the cases are in the end generated by the tactic that |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
586 |
applies the generated refutation thms (see function 'refute_tac'). |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
587 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
588 |
For variables n of type nat, a constraint 0 <= n is added. |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
589 |
*) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
590 |
|
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
591 |
(* FIXME: To optimize, the splitting of cases and the search for refutations *) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
592 |
(* could be intertwined: separate the first (fully split) case, *) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
593 |
(* refute it, continue with splitting and refuting. Terminate with *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
594 |
(* failure as soon as a case could not be refuted; i.e. delay further *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
595 |
(* splitting until after a refutation for other cases has been found. *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
596 |
|
22846 | 597 |
fun split_items sg (do_pre : bool) (Ts, terms) : |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
598 |
(typ list * (LA_Data.decompT * int) list) list = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
599 |
let |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
600 |
(* splits inequalities '~=' into '<' and '>'; this corresponds to *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
601 |
(* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
602 |
(* level *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
603 |
(* FIXME: this is currently sensitive to the order of theorems in *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
604 |
(* neqE: The theorem for type "nat" must come first. A *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
605 |
(* better (i.e. less likely to break when neqE changes) *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
606 |
(* implementation should *test* which theorem from neqE *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
607 |
(* can be applied, and split the premise accordingly. *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
608 |
fun elim_neq (ineqs : (LA_Data.decompT option * bool) list) : |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
609 |
(LA_Data.decompT option * bool) list list = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
610 |
let |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
611 |
fun elim_neq' nat_only ([] : (LA_Data.decompT option * bool) list) : |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
612 |
(LA_Data.decompT option * bool) list list = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
613 |
[[]] |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
614 |
| elim_neq' nat_only ((NONE, is_nat) :: ineqs) = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
615 |
map (cons (NONE, is_nat)) (elim_neq' nat_only ineqs) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
616 |
| elim_neq' nat_only ((ineq as (SOME (l, i, rel, r, j, d), is_nat)) :: ineqs) = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
617 |
if rel = "~=" andalso (not nat_only orelse is_nat) then |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
618 |
(* [| ?l ~= ?r; ?l < ?r ==> ?R; ?r < ?l ==> ?R |] ==> ?R *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
619 |
elim_neq' nat_only (ineqs @ [(SOME (l, i, "<", r, j, d), is_nat)]) @ |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
620 |
elim_neq' nat_only (ineqs @ [(SOME (r, j, "<", l, i, d), is_nat)]) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
621 |
else |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
622 |
map (cons ineq) (elim_neq' nat_only ineqs) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
623 |
in |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
624 |
ineqs |> elim_neq' true |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
625 |
|> map (elim_neq' false) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
626 |
|> List.concat |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
627 |
end |
13464 | 628 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
629 |
fun number_hyps _ [] = [] |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
630 |
| number_hyps n (NONE::xs) = number_hyps (n+1) xs |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
631 |
| number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
632 |
|
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
633 |
val result = (Ts, terms) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
634 |
|> (* user-defined preprocessing of the subgoal *) |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
635 |
(if do_pre then LA_Data.pre_decomp sg else Library.single) |
23195 | 636 |
|> tap (fn subgoals => trace_msg ("Preprocessing yields " ^ |
637 |
string_of_int (length subgoals) ^ " subgoal(s) total.")) |
|
22846 | 638 |
|> (* produce the internal encoding of (in-)equalities *) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
639 |
map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t)))) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
640 |
|> (* splitting of inequalities *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
641 |
map (apsnd elim_neq) |
22846 | 642 |
|> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
643 |
|> (* numbering of hypotheses, ignoring irrelevant ones *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
644 |
map (apsnd (number_hyps 0)) |
23195 | 645 |
in |
646 |
trace_msg ("Splitting of inequalities yields " ^ |
|
647 |
string_of_int (length result) ^ " subgoal(s) total."); |
|
648 |
result |
|
649 |
end; |
|
13464 | 650 |
|
20268 | 651 |
fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
652 |
(map fst lhs) union ((map fst rhs) union ats); |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
653 |
|
20268 | 654 |
fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decompT, _)) : |
655 |
(bool * term) list = |
|
656 |
(map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats); |
|
13498 | 657 |
|
20268 | 658 |
fun discr (initems : (LA_Data.decompT * int) list) : bool list = |
659 |
map fst (Library.foldl add_datoms ([],initems)); |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
660 |
|
20268 | 661 |
fun refutes (sg : theory) (params : (string * typ) list) (show_ex : bool) : |
662 |
(typ list * (LA_Data.decompT * int) list) list -> injust list -> injust list option = |
|
13498 | 663 |
let |
20268 | 664 |
fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss) |
665 |
(js : injust list) : injust list option = |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
666 |
let val atoms = Library.foldl add_atoms ([], initems) |
13498 | 667 |
val n = length atoms |
668 |
val mkleq = mklineq n atoms |
|
669 |
val ixs = 0 upto (n-1) |
|
670 |
val iatoms = atoms ~~ ixs |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
671 |
val natlineqs = List.mapPartial (mknat Ts ixs) iatoms |
13498 | 672 |
val ineqs = map mkleq initems @ natlineqs |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
673 |
in case elim (ineqs, []) of |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
674 |
Success j => |
20268 | 675 |
(trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); |
676 |
refute initemss (js@[j])) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
677 |
| Failure hist => |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
678 |
(if not show_ex then |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
679 |
() |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
680 |
else let |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
681 |
(* invent names for bound variables that are new, i.e. in Ts, *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
682 |
(* but not in params; we assume that Ts still contains (map *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
683 |
(* snd params) as a suffix *) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
684 |
val new_count = length Ts - length params - 1 |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
685 |
val new_names = map Name.bound (0 upto new_count) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
686 |
val params' = (new_names @ map fst params) ~~ Ts |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
687 |
in |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
688 |
trace_ex (sg, params', atoms, discr initems, n, hist) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
689 |
end; NONE) |
13498 | 690 |
end |
15531 | 691 |
| refute [] js = SOME js |
13498 | 692 |
in refute end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
693 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
694 |
fun refute (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
695 |
(do_pre : bool) (terms : term list) : injust list option = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
696 |
refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) []; |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
697 |
|
22950 | 698 |
fun count P xs = length (filter P xs); |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
699 |
|
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
700 |
(* The limit on the number of ~= allowed. |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
701 |
Because each ~= is split into two cases, this can lead to an explosion. |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
702 |
*) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
703 |
val fast_arith_neq_limit = ref 9; |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
704 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
705 |
fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
706 |
(do_pre : bool) (Hs : term list) (concl : term) : injust list option = |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
707 |
let |
23190 | 708 |
val _ = trace_msg "prove:" |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
709 |
(* append the negated conclusion to 'Hs' -- this corresponds to *) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
710 |
(* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
711 |
(* theorem/tactic level *) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
712 |
val Hs' = Hs @ [LA_Logic.neg_prop concl] |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
713 |
fun is_neq NONE = false |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
714 |
| is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
715 |
in |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
716 |
if count is_neq (map (LA_Data.decomp sg) Hs') |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
717 |
> !fast_arith_neq_limit then ( |
20268 | 718 |
trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ |
719 |
string_of_int (!fast_arith_neq_limit) ^ ")"); |
|
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
720 |
NONE |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
721 |
) else |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
722 |
refute sg params show_ex do_pre Hs' |
23190 | 723 |
end handle TERM ("neg_prop", _) => |
724 |
(* since no meta-logic negation is available, we can only fail if *) |
|
725 |
(* the conclusion is not of the form 'Trueprop $ _' (simply *) |
|
726 |
(* dropping the conclusion doesn't work either, because even *) |
|
727 |
(* 'False' does not imply arbitrary 'concl::prop') *) |
|
728 |
(trace_msg "prove failed (cannot negate conclusion)."; NONE); |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
729 |
|
22846 | 730 |
fun refute_tac ss (i, justs) = |
6074 | 731 |
fn state => |
20268 | 732 |
let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ |
733 |
Int.toString (length justs) ^ " justification(s)):") state |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
734 |
val sg = theory_of_thm state |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
735 |
val {neqE, ...} = Data.get sg |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
736 |
fun just1 j = |
20268 | 737 |
(* eliminate inequalities *) |
738 |
REPEAT_DETERM (eresolve_tac neqE i) THEN |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
739 |
PRIMITIVE (trace_thm "State after neqE:") THEN |
20268 | 740 |
(* use theorems generated from the actual justifications *) |
741 |
METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i |
|
742 |
in (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *) |
|
743 |
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN |
|
744 |
(* user-defined preprocessing of the subgoal *) |
|
745 |
DETERM (LA_Data.pre_tac i) THEN |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
746 |
PRIMITIVE (trace_thm "State after pre_tac:") THEN |
20268 | 747 |
(* prove every resulting subgoal, using its justification *) |
748 |
EVERY (map just1 justs) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
749 |
end state; |
6074 | 750 |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
751 |
(* |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
752 |
Fast but very incomplete decider. Only premises and conclusions |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
753 |
that are already (negated) (in)equations are taken into account. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
754 |
*) |
20268 | 755 |
fun simpset_lin_arith_tac (ss : simpset) (show_ex : bool) (i : int) (st : thm) = |
756 |
SUBGOAL (fn (A,_) => |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
757 |
let val params = rev (Logic.strip_params A) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
758 |
val Hs = Logic.strip_assums_hyp A |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
759 |
val concl = Logic.strip_assums_concl A |
12932 | 760 |
in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st; |
22578 | 761 |
case prove (Thm.theory_of_thm st) params show_ex true Hs concl of |
15531 | 762 |
NONE => (trace_msg "Refutation failed."; no_tac) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
763 |
| SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) |
9420 | 764 |
end) i st; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
765 |
|
20268 | 766 |
fun lin_arith_tac (show_ex : bool) (i : int) (st : thm) = |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
767 |
simpset_lin_arith_tac |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
768 |
(Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
769 |
show_ex i st; |
17613 | 770 |
|
20268 | 771 |
fun cut_lin_arith_tac (ss : simpset) (i : int) = |
17613 | 772 |
cut_facts_tac (Simplifier.prems_of_ss ss) i THEN |
773 |
simpset_lin_arith_tac ss false i; |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
774 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
775 |
(** Forward proof from theorems **) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
776 |
|
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
777 |
(* More tricky code. Needs to arrange the proofs of the multiple cases (due |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
778 |
to splits of ~= premises) such that it coincides with the order of the cases |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
779 |
generated by function split_items. *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
780 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
781 |
datatype splittree = Tip of thm list |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
782 |
| Spl of thm * cterm * splittree * cterm * splittree; |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
783 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
784 |
(* "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
785 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
786 |
fun extract (imp : cterm) : cterm * cterm = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
787 |
let val (Il, r) = Thm.dest_comb imp |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
788 |
val (_, imp1) = Thm.dest_comb Il |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
789 |
val (Ict1, _) = Thm.dest_comb imp1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
790 |
val (_, ct1) = Thm.dest_comb Ict1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
791 |
val (Ir, _) = Thm.dest_comb r |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
792 |
val (_, Ict2r) = Thm.dest_comb Ir |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
793 |
val (Ict2, _) = Thm.dest_comb Ict2r |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
794 |
val (_, ct2) = Thm.dest_comb Ict2 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
795 |
in (ct1, ct2) end; |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
796 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
797 |
fun splitasms (sg : theory) (asms : thm list) : splittree = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
798 |
let val {neqE, ...} = Data.get sg |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
799 |
fun elim_neq (asms', []) = Tip (rev asms') |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
800 |
| elim_neq (asms', asm::asms) = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
801 |
(case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
802 |
SOME spl => |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
803 |
let val (ct1, ct2) = extract (cprop_of spl) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
804 |
val thm1 = assume ct1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
805 |
val thm2 = assume ct2 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
806 |
in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2])) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
807 |
end |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
808 |
| NONE => elim_neq (asm::asms', asms)) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
809 |
in elim_neq ([], asms) end; |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
810 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
811 |
fun fwdproof (ctxt : theory * simpset) (Tip asms : splittree) (j::js : injust list) = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
812 |
(mkthm ctxt asms j, js) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
813 |
| fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
814 |
let val (thm1, js1) = fwdproof ctxt tree1 js |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
815 |
val (thm2, js2) = fwdproof ctxt tree2 js1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
816 |
val thm1' = implies_intr ct1 thm1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
817 |
val thm2' = implies_intr ct2 thm2 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
818 |
in (thm2' COMP (thm1' COMP thm), js2) end; |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
819 |
(* needs handle THM _ => NONE ? *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
820 |
|
20268 | 821 |
fun prover (ctxt as (sg, ss)) thms (Tconcl : term) (js : injust list) (pos : bool) : thm option = |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
822 |
let |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
823 |
(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
824 |
(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
825 |
(* but beware: this can be a significant performance issue. *) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
826 |
(* There is no "forward version" of 'pre_tac'. Therefore we combine the *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
827 |
(* available theorems into a single proof state and perform "backward proof" *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
828 |
(* using 'refute_tac'. *) |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
829 |
(* |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
830 |
val Hs = map prop_of thms |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
831 |
val Prop = fold (curry Logic.mk_implies) (rev Hs) Tconcl |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
832 |
val cProp = cterm_of sg Prop |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
833 |
val concl = Goal.init cProp |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
834 |
|> refute_tac ss (1, js) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
835 |
|> Seq.hd |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
836 |
|> Goal.finish |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
837 |
|> fold (fn thA => fn thAB => implies_elim thAB thA) thms |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
838 |
*) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
839 |
(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
840 |
val nTconcl = LA_Logic.neg_prop Tconcl |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
841 |
val cnTconcl = cterm_of sg nTconcl |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
842 |
val nTconclthm = assume cnTconcl |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
843 |
val tree = splitasms sg (thms @ [nTconclthm]) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
844 |
val (Falsethm, _) = fwdproof ctxt tree js |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
845 |
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
846 |
val concl = implies_intr cnTconcl Falsethm COMP contr |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
847 |
in SOME (trace_thm "Proved by lin. arith. prover:" |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
848 |
(LA_Logic.mk_Eq concl)) end |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
849 |
(* in case concl contains ?-var, which makes assume fail: *) |
15531 | 850 |
handle THM _ => NONE; |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
851 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
852 |
(* PRE: concl is not negated! |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
853 |
This assumption is OK because |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
854 |
1. lin_arith_prover tries both to prove and disprove concl and |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
855 |
2. lin_arith_prover is applied by the simplifier which |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
856 |
dives into terms and will thus try the non-negated concl anyway. |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
857 |
*) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
858 |
|
20268 | 859 |
fun lin_arith_prover sg ss (concl : term) : thm option = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
860 |
let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss)); |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
861 |
val Hs = map prop_of thms |
6102 | 862 |
val Tconcl = LA_Logic.mk_Trueprop concl |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
863 |
(* |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
864 |
val _ = trace_msg "lin_arith_prover" |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
865 |
val _ = map (trace_thm "thms:") thms |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
866 |
val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
867 |
*) |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
868 |
in case prove sg [] false false Hs Tconcl of (* concl provable? *) |
17515 | 869 |
SOME js => prover (sg, ss) thms Tconcl js true |
15531 | 870 |
| NONE => let val nTconcl = LA_Logic.neg_prop Tconcl |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
871 |
in case prove sg [] false false Hs nTconcl of (* ~concl provable? *) |
17515 | 872 |
SOME js => prover (sg, ss) thms nTconcl js false |
15531 | 873 |
| NONE => NONE |
6079 | 874 |
end |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
875 |
end; |
6074 | 876 |
|
877 |
end; |