author | nipkow |
Tue, 03 Feb 2004 10:19:21 +0100 | |
changeset 14372 | 51ddf8963c95 |
parent 14360 | e654599b114e |
child 14386 | ad1ffcc90162 |
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 |
||
14 |
lin_arith_prover: Sign.sg -> thm list -> term -> thm option |
|
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 |
|
26 |
val conjI: thm |
|
27 |
val ccontr: thm (* (~ P ==> False) ==> P *) |
|
28 |
val neqE: thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *) |
|
29 |
val notI: thm (* (P ==> False) ==> ~ P *) |
|
6110 | 30 |
val not_lessD: thm (* ~(m < n) ==> n <= m *) |
6128 | 31 |
val not_leD: thm (* ~(m <= n) ==> n < m *) |
6102 | 32 |
val sym: thm (* x = y ==> y = x *) |
33 |
val mk_Eq: thm -> thm |
|
34 |
val mk_Trueprop: term -> term |
|
35 |
val neg_prop: term -> term |
|
36 |
val is_False: thm -> bool |
|
6128 | 37 |
val is_nat: typ list * term -> bool |
38 |
val mk_nat_thm: Sign.sg -> 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 |
||
45 |
neg_prop(t) = neg if t is wrapped up in Trueprop and |
|
46 |
nt is the (logically) negated version of t, where the negation |
|
47 |
of a negative term is the term itself (no double negation!); |
|
6128 | 48 |
|
49 |
is_nat(parameter-types,t) = t:nat |
|
50 |
mk_nat_thm(t) = "0 <= t" |
|
6102 | 51 |
*) |
52 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
53 |
signature LIN_ARITH_DATA = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
54 |
sig |
6128 | 55 |
val decomp: |
10691 | 56 |
Sign.sg -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option |
57 |
val number_of: int * typ -> term |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
58 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
59 |
(* |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
60 |
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
|
61 |
where Rel is one of "<", "~<", "<=", "~<=" and "=" and |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
62 |
p/q is the decomposition of the sum terms x/y into a list |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
63 |
of summand * multiplicity pairs and a constant summand and |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
64 |
d indicates if the domain is discrete. |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
65 |
|
9420 | 66 |
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
|
67 |
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
|
68 |
otherwise <= can grow to massive proportions. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
69 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
70 |
|
6062 | 71 |
signature FAST_LIN_ARITH = |
72 |
sig |
|
9420 | 73 |
val setup: (theory -> theory) list |
10691 | 74 |
val map_data: ({add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, |
10575 | 75 |
lessD: thm list, simpset: Simplifier.simpset} |
10691 | 76 |
-> {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, |
10575 | 77 |
lessD: thm list, simpset: Simplifier.simpset}) |
78 |
-> theory -> theory |
|
9073 | 79 |
val trace : bool ref |
6074 | 80 |
val lin_arith_prover: Sign.sg -> thm list -> term -> thm option |
13498 | 81 |
val lin_arith_tac: bool -> int -> tactic |
6062 | 82 |
val cut_lin_arith_tac: thm list -> int -> tactic |
83 |
end; |
|
84 |
||
6102 | 85 |
functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC |
86 |
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
|
87 |
struct |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
88 |
|
9420 | 89 |
|
90 |
(** theory data **) |
|
91 |
||
92 |
(* data kind 'Provers/fast_lin_arith' *) |
|
93 |
||
94 |
structure DataArgs = |
|
95 |
struct |
|
96 |
val name = "Provers/fast_lin_arith"; |
|
10691 | 97 |
type T = {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, |
10575 | 98 |
lessD: thm list, simpset: Simplifier.simpset}; |
9420 | 99 |
|
10691 | 100 |
val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], |
10575 | 101 |
lessD = [], simpset = Simplifier.empty_ss}; |
9420 | 102 |
val copy = I; |
103 |
val prep_ext = I; |
|
104 |
||
10691 | 105 |
fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, |
10575 | 106 |
lessD = lessD1, simpset = simpset1}, |
10691 | 107 |
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, |
10575 | 108 |
lessD = lessD2, simpset = simpset2}) = |
9420 | 109 |
{add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), |
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12932
diff
changeset
|
110 |
mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst) |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12932
diff
changeset
|
111 |
mult_mono_thms1 mult_mono_thms2, |
10575 | 112 |
inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), |
113 |
lessD = Drule.merge_rules (lessD1, lessD2), |
|
114 |
simpset = Simplifier.merge_ss (simpset1, simpset2)}; |
|
9420 | 115 |
|
116 |
fun print _ _ = (); |
|
117 |
end; |
|
118 |
||
119 |
structure Data = TheoryDataFun(DataArgs); |
|
120 |
val map_data = Data.map; |
|
121 |
val setup = [Data.init]; |
|
122 |
||
123 |
||
124 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
125 |
(*** A fast decision procedure ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
126 |
(*** Code ported from HOL Light ***) |
6056 | 127 |
(* possible optimizations: |
128 |
use (var,coeff) rep or vector rep tp save space; |
|
129 |
treat non-negative atoms separately rather than adding 0 <= atom |
|
130 |
*) |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
131 |
|
9073 | 132 |
val trace = ref false; |
133 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
134 |
datatype lineq_type = Eq | Le | Lt; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
135 |
|
6056 | 136 |
datatype injust = Asm of int |
137 |
| Nat of int (* index of atom *) |
|
6128 | 138 |
| LessD of injust |
139 |
| NotLessD of injust |
|
140 |
| NotLeD of injust |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
141 |
| NotLeDD of injust |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
142 |
| Multiplied of int * injust |
10691 | 143 |
| Multiplied2 of int * injust |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
144 |
| Added of injust * injust; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
145 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
146 |
datatype lineq = Lineq of int * lineq_type * int list * injust; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
147 |
|
13498 | 148 |
fun el 0 (h::_) = h |
149 |
| el n (_::t) = el (n - 1) t |
|
150 |
| el _ _ = sys_error "el"; |
|
151 |
||
152 |
(* ------------------------------------------------------------------------- *) |
|
153 |
(* Finding a (counter) example from the trace of a failed elimination *) |
|
154 |
(* ------------------------------------------------------------------------- *) |
|
155 |
(* Examples are represented as rational numbers, *) |
|
156 |
(* Dont blame John Harrison for this code - it is entirely mine. TN *) |
|
157 |
||
158 |
exception NoEx; |
|
159 |
||
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
160 |
(* 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
|
161 |
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
|
162 |
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
|
163 |
*) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
164 |
|
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
165 |
fun elim_eqns(ineqs,Lineq(i,Le,cs,_)) = (i,true,cs)::ineqs |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
166 |
| elim_eqns(ineqs,Lineq(i,Eq,cs,_)) = (i,true,cs)::(~i,true,map ~ cs)::ineqs |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
167 |
| elim_eqns(ineqs,Lineq(i,Lt,cs,_)) = (i,false,cs)::ineqs; |
13498 | 168 |
|
169 |
val rat0 = rat_of_int 0; |
|
170 |
||
171 |
(* PRE: ex[v] must be 0! *) |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
172 |
fun eval (ex:rat list) v (a:int,le,cs:int list) = |
13498 | 173 |
let val rs = map rat_of_int cs |
174 |
val rsum = foldl ratadd (rat0,map ratmul (rs ~~ ex)) |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
175 |
in (ratmul(ratadd(rat_of_int a,ratneg rsum), ratinv(el v rs)), le) end; |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
176 |
(* If el v rs < 0, le should be negated. |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
177 |
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
|
178 |
*) |
13498 | 179 |
|
180 |
fun ratge0 r = fst(rep_rat r) >= 0; |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
181 |
fun ratle(r,s) = ratge0(ratadd(s,ratneg r)); |
13498 | 182 |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
183 |
fun ratrelmin2(x as (r,ler),y as (s,les)) = |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
184 |
if r=s then (r, (not ler) andalso (not les)) else if ratle(r,s) then x else y; |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
185 |
fun ratrelmax2(x as (r,ler),y as (s,les)) = |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
186 |
if r=s then (r,ler andalso les) else if ratle(r,s) then y else x; |
13498 | 187 |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
188 |
val ratrelmin = foldr1 ratrelmin2; |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
189 |
val ratrelmax = foldr1 ratrelmax2; |
13498 | 190 |
|
191 |
fun ratroundup r = let val (p,q) = rep_rat r |
|
192 |
in if q=1 then r else rat_of_int((p div q) + 1) end |
|
193 |
||
194 |
fun ratrounddown r = let val (p,q) = rep_rat r |
|
195 |
in if q=1 then r else rat_of_int((p div q) - 1) end |
|
196 |
||
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
197 |
fun ratexact up (r,exact) = |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
198 |
if exact then r else |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
199 |
let val (p,q) = rep_rat r |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
200 |
val nth = ratinv(rat_of_int q) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
201 |
in ratadd(r,if up then nth else ratneg nth) end; |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
202 |
|
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
203 |
fun ratmiddle(r,s) = ratmul(ratadd(r,s),ratinv(rat_of_int 2)); |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
204 |
|
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
205 |
fun choose2 d ((lb,exactl),(ub,exactu)) = |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
206 |
if ratle(lb,rat0) andalso (lb <> rat0 orelse exactl) andalso |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
207 |
ratle(rat0,ub) andalso (ub <> rat0 orelse exactu) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
208 |
then rat0 else |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
209 |
if not d |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
210 |
then (if ratge0 lb |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
211 |
then if exactl then lb else ratmiddle(lb,ub) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
212 |
else if exactu then ub else ratmiddle(lb,ub)) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
213 |
else (* discrete domain, both bounds must be exact *) |
13498 | 214 |
if ratge0 lb then let val lb' = ratroundup lb |
215 |
in if ratle(lb',ub) then lb' else raise NoEx end |
|
216 |
else let val ub' = ratrounddown ub |
|
217 |
in if ratle(lb,ub') then ub' else raise NoEx end; |
|
218 |
||
219 |
fun findex1 discr (ex,(v,lineqs)) = |
|
220 |
let val nz = filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs; |
|
221 |
val ineqs = foldl elim_eqns ([],nz) |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
222 |
val (ge,le) = partition (fn (_,_,cs) => el v cs > 0) ineqs |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
223 |
val lb = ratrelmax(map (eval ex v) ge) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
224 |
val ub = ratrelmin(map (eval ex v) le) |
13498 | 225 |
in nth_update (choose2 (nth_elem(v,discr)) (lb,ub)) (v,ex) end; |
226 |
||
227 |
fun findex discr = foldl (findex1 discr); |
|
228 |
||
229 |
fun elim1 v x = |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
230 |
map (fn (a,le,bs) => (ratadd(a,ratneg(ratmul(el v bs,x))), le, |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
231 |
nth_update rat0 (v,bs))); |
13498 | 232 |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
233 |
fun single_var v (_,_,cs) = (filter_out (equal rat0) cs = [el v cs]); |
13498 | 234 |
|
235 |
(* The base case: |
|
236 |
all variables occur only with positive or only with negative coefficients *) |
|
237 |
fun pick_vars discr (ineqs,ex) = |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
238 |
let val nz = filter_out (fn (_,_,cs) => forall (equal rat0) cs) ineqs |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
239 |
in case nz of [] => ex |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
240 |
| (_,_,cs) :: _ => |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
241 |
let val v = find_index (not o equal rat0) cs |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
242 |
val d = nth_elem(v,discr) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
243 |
val pos = ratge0(el v cs) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
244 |
val sv = filter (single_var v) nz |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
245 |
val minmax = |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
246 |
if pos then if d then ratroundup o fst o ratrelmax |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
247 |
else ratexact true o ratrelmax |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
248 |
else if d then ratrounddown o fst o ratrelmin |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
249 |
else ratexact false o ratrelmin |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
250 |
val bnds = map (fn (a,le,bs) => (ratmul(a,ratinv(el v bs)),le)) sv |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
251 |
val x = minmax((rat0,if pos then true else false)::bnds) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
252 |
val ineqs' = elim1 v x nz |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
253 |
val ex' = nth_update x (v,ex) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
254 |
in pick_vars discr (ineqs',ex') end |
13498 | 255 |
end; |
256 |
||
257 |
fun findex0 discr n lineqs = |
|
258 |
let val ineqs = foldl elim_eqns ([],lineqs) |
|
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
259 |
val rineqs = map (fn (a,le,cs) => (rat_of_int a, le, map rat_of_int cs)) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
260 |
ineqs |
13498 | 261 |
in pick_vars discr (rineqs,replicate n rat0) end; |
262 |
||
263 |
(* ------------------------------------------------------------------------- *) |
|
264 |
(* End of counter example finder. The actual decision procedure starts here. *) |
|
265 |
(* ------------------------------------------------------------------------- *) |
|
266 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
267 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
268 |
(* 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
|
269 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
270 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
271 |
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
|
272 |
| find_add_type(x,Eq) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
273 |
| find_add_type(_,Lt) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
274 |
| find_add_type(Lt,_) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
275 |
| find_add_type(Le,Le) = Le; |
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 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
278 |
(* Multiply out an (in)equation. *) |
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 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
281 |
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
|
282 |
if n = 1 then i |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
283 |
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
|
284 |
else if n < 0 andalso (ty=Le orelse 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
|
285 |
else Lineq(n * k,ty,map (apl(n,op * )) l,Multiplied(n,just)); |
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 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
288 |
(* Add together (in)equations. *) |
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 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
291 |
fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
292 |
let val l = map2 (op +) (l1,l2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
293 |
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
|
294 |
|
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 |
(* 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
|
297 |
(* 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
|
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 elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
301 |
let val c1 = el v l1 and c2 = el v l2 |
10691 | 302 |
val m = lcm(abs c1,abs c2) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
303 |
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
|
304 |
val (n1,n2) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
305 |
if (c1 >= 0) = (c2 >= 0) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
306 |
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
|
307 |
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
|
308 |
else sys_error "elim_var" |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
309 |
else (m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
310 |
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
|
311 |
then (~n1,~n2) else (n1,n2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
312 |
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
|
313 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
314 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
315 |
(* The main refutation-finding code. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
316 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
317 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
318 |
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
|
319 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
320 |
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
|
321 |
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
|
322 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
323 |
fun calc_blowup l = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
324 |
let val (p,n) = partition (apl(0,op<)) (filter (apl(0,op<>)) l) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
325 |
in (length p) * (length n) end; |
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 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
328 |
(* Main elimination code: *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
329 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
330 |
(* (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
|
331 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
332 |
(* (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
|
333 |
(* 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
|
334 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
335 |
(* (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
|
336 |
(* 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
|
337 |
(* ------------------------------------------------------------------------- *) |
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 |
fun allpairs f xs ys = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
340 |
flat(map (fn x => map (fn y => f x y) ys) xs); |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
341 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
342 |
fun extract_first p = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
343 |
let fun extract xs (y::ys) = if p y then (Some y,xs@ys) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
344 |
else extract (y::xs) ys |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
345 |
| extract xs [] = (None,xs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
346 |
in extract [] end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
347 |
|
6056 | 348 |
fun print_ineqs ineqs = |
9073 | 349 |
if !trace then |
12262 | 350 |
tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => |
9073 | 351 |
string_of_int c ^ |
352 |
(case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ |
|
353 |
commas(map string_of_int l)) ineqs)) |
|
354 |
else (); |
|
6056 | 355 |
|
13498 | 356 |
type history = (int * lineq list) list; |
357 |
datatype result = Success of injust | Failure of history; |
|
358 |
||
359 |
fun elim(ineqs,hist) = |
|
9073 | 360 |
let val dummy = print_ineqs ineqs; |
6056 | 361 |
val (triv,nontriv) = partition is_trivial ineqs in |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
362 |
if not(null triv) |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
363 |
then case Library.find_first is_answer triv of |
13498 | 364 |
None => elim(nontriv,hist) |
365 |
| Some(Lineq(_,_,_,j)) => Success j |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
366 |
else |
13498 | 367 |
if null nontriv then Failure(hist) |
368 |
else |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
369 |
let val (eqs,noneqs) = partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
370 |
if not(null eqs) then |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
371 |
let val clist = foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
372 |
val sclist = sort (fn (x,y) => int_ord(abs(x),abs(y))) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
373 |
(filter (fn i => i<>0) clist) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
374 |
val c = hd sclist |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
375 |
val (Some(eq as Lineq(_,_,ceq,_)),othereqs) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
376 |
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs |
13498 | 377 |
val v = find_index_eq c ceq |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
378 |
val (ioth,roth) = partition (fn (Lineq(_,_,l,_)) => el v l = 0) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
379 |
(othereqs @ noneqs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
380 |
val others = map (elim_var v eq) roth @ ioth |
13498 | 381 |
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
|
382 |
else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
383 |
let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
384 |
val numlist = 0 upto (length(hd lists) - 1) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
385 |
val coeffs = map (fn i => map (el i) lists) numlist |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
386 |
val blows = map calc_blowup coeffs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
387 |
val iblows = blows ~~ numlist |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
388 |
val nziblows = filter (fn (i,_) => i<>0) iblows |
13498 | 389 |
in if null nziblows then Failure((~1,nontriv)::hist) |
390 |
else |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
391 |
let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
392 |
val (no,yes) = partition (fn (Lineq(_,_,l,_)) => el v l = 0) ineqs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
393 |
val (pos,neg) = partition(fn (Lineq(_,_,l,_)) => el v l > 0) yes |
13498 | 394 |
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
|
395 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
396 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
397 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
398 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
399 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
400 |
(* Translate back a proof. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
401 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
402 |
|
9073 | 403 |
fun trace_thm msg th = |
12262 | 404 |
if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th; |
9073 | 405 |
|
406 |
fun trace_msg msg = |
|
12262 | 407 |
if !trace then tracing msg else (); |
9073 | 408 |
|
13498 | 409 |
(* FIXME OPTIMIZE!!!! (partly done already) |
6056 | 410 |
Addition/Multiplication need i*t representation rather than t+t+... |
10691 | 411 |
Get rid of Mulitplied(2). For Nat LA_Data.number_of should return Suc^n |
412 |
because Numerals are not known early enough. |
|
6056 | 413 |
|
414 |
Simplification may detect a contradiction 'prematurely' due to type |
|
415 |
information: n+1 <= 0 is simplified to False and does not need to be crossed |
|
416 |
with 0 <= n. |
|
417 |
*) |
|
418 |
local |
|
419 |
exception FalseE of thm |
|
420 |
in |
|
6074 | 421 |
fun mkthm sg asms just = |
10691 | 422 |
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} = Data.get_sg sg; |
9420 | 423 |
val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) => |
6056 | 424 |
map fst lhs union (map fst rhs union ats)) |
13464 | 425 |
([], mapfilter (fn thm => if Thm.no_prems thm |
426 |
then LA_Data.decomp sg (concl_of thm) |
|
427 |
else None) asms) |
|
6056 | 428 |
|
10575 | 429 |
fun add2 thm1 thm2 = |
6102 | 430 |
let val conj = thm1 RS (thm2 RS LA_Logic.conjI) |
10575 | 431 |
in get_first (fn th => Some(conj RS th) handle _ => None) add_mono_thms |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
432 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
433 |
|
10575 | 434 |
fun try_add [] _ = None |
435 |
| try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of |
|
436 |
None => try_add thm1s thm2 | some => some; |
|
437 |
||
438 |
fun addthms thm1 thm2 = |
|
439 |
case add2 thm1 thm2 of |
|
440 |
None => (case try_add ([thm1] RL inj_thms) thm2 of |
|
14360 | 441 |
None => ( the(try_add ([thm2] RL inj_thms) thm1) |
442 |
handle OPTION => |
|
443 |
(trace_thm "" thm1; trace_thm "" thm2; |
|
444 |
sys_error "Lin.arith. failed to add thms") |
|
445 |
) |
|
10575 | 446 |
| Some thm => thm) |
447 |
| Some thm => thm; |
|
448 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
449 |
fun multn(n,thm) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
450 |
let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th) |
6102 | 451 |
in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
452 |
|
10691 | 453 |
fun multn2(n,thm) = |
454 |
let val Some(mth,cv) = |
|
455 |
get_first (fn (th,cv) => Some(thm RS th,cv) handle _ => None) mult_mono_thms |
|
456 |
val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv))) |
|
457 |
in instantiate ([],[(cv,ct)]) mth end |
|
458 |
||
6056 | 459 |
fun simp thm = |
12932 | 460 |
let val thm' = trace_thm "Simplified:" (full_simplify simpset thm) |
6102 | 461 |
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end |
6056 | 462 |
|
9073 | 463 |
fun mk(Asm i) = trace_thm "Asm" (nth_elem(i,asms)) |
13464 | 464 |
| mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) |
9420 | 465 |
| mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD)) |
9073 | 466 |
| mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
9420 | 467 |
| mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD)) |
9073 | 468 |
| mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
469 |
| mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) |
|
10717 | 470 |
| mk(Multiplied(n,j)) = (trace_msg("*"^string_of_int n); trace_thm "*" (multn(n,mk j))) |
471 |
| mk(Multiplied2(n,j)) = simp (trace_msg("**"^string_of_int 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
|
472 |
|
9073 | 473 |
in trace_msg "mkthm"; |
12932 | 474 |
let val thm = trace_thm "Final thm:" (mk just) |
475 |
in let val fls = simplify simpset thm |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
476 |
in trace_thm "After simplification:" fls; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
477 |
if LA_Logic.is_False fls then fls |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
478 |
else |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
479 |
(tracing "Assumptions:"; seq print_thm asms; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
480 |
tracing "Proved:"; print_thm fls; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
481 |
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
|
482 |
\Please inform Tobias Nipkow (nipkow@in.tum.de)."; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
483 |
fls) |
12932 | 484 |
end |
485 |
end handle FalseE thm => (trace_thm "False reached early:" thm; thm) |
|
486 |
end |
|
6056 | 487 |
end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
488 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
489 |
fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
490 |
|
10691 | 491 |
fun lcms is = foldl lcm (1,is); |
492 |
||
493 |
fun integ(rlhs,r,rel,rrhs,s,d) = |
|
494 |
let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s |
|
495 |
val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)) |
|
496 |
fun mult(t,r) = let val (i,j) = rep_rat r in (t,i * (m div j)) end |
|
12932 | 497 |
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end |
10691 | 498 |
|
13498 | 499 |
fun mklineq n atoms = |
500 |
fn (item,k) => |
|
501 |
let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item |
|
502 |
val lhsa = map (coeff lhs) atoms |
|
503 |
and rhsa = map (coeff rhs) atoms |
|
504 |
val diff = map2 (op -) (rhsa,lhsa) |
|
505 |
val c = i-j |
|
506 |
val just = Asm k |
|
507 |
fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j)) |
|
508 |
in case rel of |
|
509 |
"<=" => lineq(c,Le,diff,just) |
|
510 |
| "~<=" => if discrete |
|
511 |
then lineq(1-c,Le,map (op ~) diff,NotLeDD(just)) |
|
512 |
else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) |
|
513 |
| "<" => if discrete |
|
514 |
then lineq(c+1,Le,diff,LessD(just)) |
|
515 |
else lineq(c,Lt,diff,just) |
|
516 |
| "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just)) |
|
517 |
| "=" => lineq(c,Eq,diff,just) |
|
518 |
| _ => sys_error("mklineq" ^ rel) |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
519 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
520 |
|
13498 | 521 |
(* ------------------------------------------------------------------------- *) |
522 |
(* Print (counter) example *) |
|
523 |
(* ------------------------------------------------------------------------- *) |
|
524 |
||
525 |
fun print_atom((a,d),r) = |
|
526 |
let val (p,q) = rep_rat r |
|
527 |
val s = if d then string_of_int p else |
|
528 |
if p = 0 then "0" |
|
529 |
else string_of_int p ^ "/" ^ string_of_int q |
|
530 |
in a ^ " = " ^ s end; |
|
531 |
||
532 |
fun print_ex sds = |
|
533 |
tracing o |
|
534 |
apl("Counter example:\n",op ^) o |
|
535 |
commas o |
|
536 |
map print_atom o |
|
537 |
apl(sds, op ~~); |
|
538 |
||
539 |
fun trace_ex(sg,params,atoms,discr,n,hist:history) = |
|
540 |
if null hist then () |
|
541 |
else let val frees = map Free params; |
|
542 |
fun s_of_t t = Sign.string_of_term sg (subst_bounds(frees,t)); |
|
543 |
val (v,lineqs) :: hist' = hist |
|
544 |
val start = if v = ~1 then (findex0 discr n lineqs,hist') |
|
545 |
else (replicate n rat0,hist) |
|
13516 | 546 |
in warning "arith failed - see trace for a counter example"; |
547 |
print_ex ((map s_of_t atoms)~~discr) (findex discr start) |
|
13498 | 548 |
handle NoEx => |
549 |
(tracing "The decision procedure failed to prove your proposition\n\ |
|
550 |
\but could not construct a counter example either.\n\ |
|
551 |
\Probably the proposition is true but cannot be proved\n\ |
|
552 |
\by the incomplete decision procedure.") |
|
553 |
end |
|
554 |
handle NotYetImpl => |
|
555 |
tracing "No counter example: < on real not yet implemented."; |
|
556 |
||
6056 | 557 |
fun mknat pTs ixs (atom,i) = |
6128 | 558 |
if LA_Logic.is_nat(pTs,atom) |
6056 | 559 |
then let val l = map (fn j => if j=i then 1 else 0) ixs |
560 |
in Some(Lineq(0,Le,l,Nat(i))) end |
|
561 |
else None |
|
562 |
||
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
563 |
(* This code is tricky. It takes a list of premises in the order they occur |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
564 |
in the subgoal. Numerical premises are coded as Some(tuple), non-numerical |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
565 |
ones as None. Going through the premises, each numeric one is converted into |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
566 |
a Lineq. The tricky bit is to convert ~= which is split into two cases < and |
13498 | 567 |
>. 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
|
568 |
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
|
569 |
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
|
570 |
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
|
571 |
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
|
572 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
573 |
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
|
574 |
*) |
13464 | 575 |
fun split_items(items) = |
576 |
let fun elim_neq front _ [] = [rev front] |
|
577 |
| elim_neq front n (None::ineqs) = elim_neq front (n+1) ineqs |
|
578 |
| elim_neq front n (Some(ineq as (l,i,rel,r,j,d))::ineqs) = |
|
579 |
if rel = "~=" then elim_neq front n (ineqs @ [Some(l,i,"<",r,j,d)]) @ |
|
580 |
elim_neq front n (ineqs @ [Some(r,j,"<",l,i,d)]) |
|
581 |
else elim_neq ((ineq,n) :: front) (n+1) ineqs |
|
582 |
in elim_neq [] 0 items end; |
|
583 |
||
13498 | 584 |
fun add_atoms(ats,((lhs,_,_,rhs,_,_),_)) = |
585 |
(map fst lhs) union ((map fst rhs) union ats) |
|
13464 | 586 |
|
13498 | 587 |
fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) = |
588 |
(map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats) |
|
589 |
||
590 |
fun discr initems = map fst (foldl add_datoms ([],initems)); |
|
13464 | 591 |
|
13498 | 592 |
fun refutes sg (pTs,params) ex = |
593 |
let |
|
594 |
fun refute (initems::initemss) js = |
|
595 |
let val atoms = foldl add_atoms ([],initems) |
|
596 |
val n = length atoms |
|
597 |
val mkleq = mklineq n atoms |
|
598 |
val ixs = 0 upto (n-1) |
|
599 |
val iatoms = atoms ~~ ixs |
|
600 |
val natlineqs = mapfilter (mknat pTs ixs) iatoms |
|
601 |
val ineqs = map mkleq initems @ natlineqs |
|
602 |
in case elim(ineqs,[]) of |
|
603 |
Success(j) => |
|
604 |
(trace_msg "Contradiction!"; refute initemss (js@[j])) |
|
605 |
| Failure(hist) => |
|
606 |
(if not ex then () |
|
607 |
else trace_ex(sg,params,atoms,discr initems,n,hist); |
|
608 |
None) |
|
609 |
end |
|
610 |
| refute [] js = Some js |
|
611 |
in refute end; |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
612 |
|
13498 | 613 |
fun refute sg ps ex items = refutes sg ps ex (split_items items) []; |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
614 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
615 |
fun refute_tac(i,justs) = |
6074 | 616 |
fn state => |
617 |
let val sg = #sign(rep_thm state) |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
618 |
fun just1 j = REPEAT_DETERM(etac LA_Logic.neqE i) THEN |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
619 |
METAHYPS (fn asms => rtac (mkthm sg asms j) 1) i |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
620 |
in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
621 |
EVERY(map just1 justs) |
6074 | 622 |
end |
623 |
state; |
|
624 |
||
13498 | 625 |
fun prove sg ps ex Hs concl = |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
626 |
let val Hitems = map (LA_Data.decomp sg) Hs |
9420 | 627 |
in case LA_Data.decomp sg concl of |
13498 | 628 |
None => refute sg ps ex (Hitems@[None]) |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
629 |
| Some(citem as (r,i,rel,l,j,d)) => |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
630 |
let val neg::rel0 = explode rel |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
631 |
val nrel = if neg = "~" then implode rel0 else "~"^rel |
13498 | 632 |
in refute sg ps ex (Hitems @ [Some(r,i,nrel,l,j,d)]) end |
6074 | 633 |
end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
634 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
635 |
(* |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
636 |
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
|
637 |
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
|
638 |
*) |
13498 | 639 |
fun lin_arith_tac ex i st = SUBGOAL (fn (A,_) => |
640 |
let val params = rev(Logic.strip_params A) |
|
641 |
val pTs = map snd params |
|
6056 | 642 |
val Hs = Logic.strip_assums_hyp A |
6074 | 643 |
val concl = Logic.strip_assums_concl A |
12932 | 644 |
in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st; |
13498 | 645 |
case prove (Thm.sign_of_thm st) (pTs,params) ex Hs concl of |
13464 | 646 |
None => (trace_msg "Refutation failed."; no_tac) |
647 |
| Some js => (trace_msg "Refutation succeeded."; refute_tac(i,js)) |
|
9420 | 648 |
end) i st; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
649 |
|
13498 | 650 |
fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac false i; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
651 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
652 |
(** Forward proof from theorems **) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
653 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
654 |
(* More tricky code. Needs to arrange the proofs of the multiple cases (due |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
655 |
to splits of ~= premises) such that it coincides with the order of the cases |
13498 | 656 |
generated by function split_items. *) |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
657 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
658 |
datatype splittree = Tip of thm list |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
659 |
| Spl of thm * cterm * splittree * cterm * splittree |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
660 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
661 |
fun extract imp = |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
662 |
let val (Il,r) = Thm.dest_comb imp |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
663 |
val (_,imp1) = Thm.dest_comb Il |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
664 |
val (Ict1,_) = Thm.dest_comb imp1 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
665 |
val (_,ct1) = Thm.dest_comb Ict1 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
666 |
val (Ir,_) = Thm.dest_comb r |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
667 |
val (_,Ict2r) = Thm.dest_comb Ir |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
668 |
val (Ict2,_) = Thm.dest_comb Ict2r |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
669 |
val (_,ct2) = Thm.dest_comb Ict2 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
670 |
in (ct1,ct2) end; |
6074 | 671 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
672 |
fun splitasms asms = |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
673 |
let fun split(asms',[]) = Tip(rev asms') |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
674 |
| split(asms',asm::asms) = |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
675 |
let val spl = asm COMP LA_Logic.neqE |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
676 |
val (ct1,ct2) = extract(cprop_of spl) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
677 |
val thm1 = assume ct1 and thm2 = assume ct2 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
678 |
in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2])) end |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
679 |
handle THM _ => split(asm::asms', asms) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
680 |
in split([],asms) end; |
6074 | 681 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
682 |
fun fwdproof sg (Tip asms) (j::js) = (mkthm sg asms j, js) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
683 |
| fwdproof sg (Spl(thm,ct1,tree1,ct2,tree2)) js = |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
684 |
let val (thm1,js1) = fwdproof sg tree1 js |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
685 |
val (thm2,js2) = fwdproof sg tree2 js1 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
686 |
val thm1' = implies_intr ct1 thm1 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
687 |
val thm2' = implies_intr ct2 thm2 |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
688 |
in (thm2' COMP (thm1' COMP thm), js2) end; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
689 |
(* needs handle _ => None ? *) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
690 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
691 |
fun prover sg thms Tconcl js pos = |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
692 |
let val nTconcl = LA_Logic.neg_prop Tconcl |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
693 |
val cnTconcl = cterm_of sg nTconcl |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
694 |
val nTconclthm = assume cnTconcl |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
695 |
val tree = splitasms (thms @ [nTconclthm]) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
696 |
val (thm,_) = fwdproof sg tree js |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
697 |
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
698 |
in Some(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
699 |
(* in case concl contains ?-var, which makes assume fail: *) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
700 |
handle THM _ => None; |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
701 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
702 |
(* PRE: concl is not negated! |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
703 |
This assumption is OK because |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
704 |
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
|
705 |
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
|
706 |
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
|
707 |
*) |
6074 | 708 |
fun lin_arith_prover sg thms concl = |
709 |
let val Hs = map (#prop o rep_thm) thms |
|
6102 | 710 |
val Tconcl = LA_Logic.mk_Trueprop concl |
13498 | 711 |
in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *) |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
712 |
Some js => prover sg thms Tconcl js true |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
713 |
| None => let val nTconcl = LA_Logic.neg_prop Tconcl |
13498 | 714 |
in case prove sg ([],[]) false Hs nTconcl of (* ~concl provable? *) |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
715 |
Some js => prover sg thms nTconcl js false |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
716 |
| None => None |
6079 | 717 |
end |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
718 |
end; |
6074 | 719 |
|
720 |
end; |