author  wenzelm 
Tue, 31 Jul 2007 00:56:29 +0200  
changeset 24076  ae946f751c44 
parent 24039  273698405054 
child 24112  6c4e7d17f9b0 
permissions  rwrr 
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$ 
24076  3 
Author: Tobias Nipkow and Tjark Weber 
6102  4 

24076  5 
A generic linear arithmetic package. It provides two tactics 
6 
(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure 

7 
(lin_arith_simproc). 

6102  8 

24076  9 
Only take premises and conclusions into account that are already 
10 
(negated) (in)equations. lin_arith_simproc tries to prove or disprove 

11 
the term. 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

12 
*) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

13 

9073  14 
(* Debugging: set Fast_Arith.trace *) 
7582  15 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

16 
(*** 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

17 

6102  18 
signature LIN_ARITH_LOGIC = 
19 
sig 

20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

20 
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

21 
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

22 
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

23 
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

24 
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

25 
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

26 
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

27 
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

28 
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

29 
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

30 
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

31 
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

32 
val mk_nat_thm : theory > term > thm 
6102  33 
end; 
34 
(* 

35 
mk_Eq(~in) = `in == False' 

36 
mk_Eq(in) = `in == True' 

37 
where `in' is an (in)equality. 

38 

23190  39 
neg_prop(t) = neg if t is wrapped up in Trueprop and neg is the 
40 
(logically) negated version of t (again wrapped up in Trueprop), 

41 
where the negation of a negative term is the term itself (no 

42 
double negation!); raises TERM ("neg_prop", [t]) if t is not of 

43 
the form 'Trueprop $ _' 

6128  44 

45 
is_nat(parametertypes,t) = t:nat 

46 
mk_nat_thm(t) = "0 <= t" 

6102  47 
*) 
48 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

49 
signature LIN_ARITH_DATA = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

50 
sig 
24076  51 
(*internal representation of linear (in)equations:*) 
20268  52 
type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool 
24076  53 
val decomp: Proof.context > term > decompT option 
54 
val domain_is_nat: term > bool 

55 

56 
(*preprocessing, performed on a representation of subgoals as list of premises:*) 

57 
val pre_decomp: Proof.context > typ list * term list > (typ list * term list) list 

58 

59 
(*preprocessing, performed on the goal  must do the same as 'pre_decomp':*) 

60 
val pre_tac: Proof.context > int > tactic 

61 
val number_of: IntInf.int * typ > term 

62 

63 
(*the limit on the number of ~= allowed; because each ~= is split 

64 
into two cases, this can lead to an explosion*) 

65 
val fast_arith_neq_limit: int ConfigOption.T 

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 nondistrete 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 
betaequivalent 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}) 
24076  95 
> Context.generic > Context.generic 
19314  96 
val trace: bool ref 
17613  97 
val cut_lin_arith_tac: simpset > int > tactic 
24076  98 
val lin_arith_tac: Proof.context > bool > int > tactic 
99 
val lin_arith_simproc: simpset > term > thm option 

6062  100 
end; 
101 

24076  102 
functor Fast_Lin_Arith 
103 
(structure LA_Logic: LIN_ARITH_LOGIC 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

104 
struct 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

105 

9420  106 

107 
(** theory data **) 

108 

24076  109 
structure Data = GenericDataFun 
22846  110 
( 
24076  111 
type T = 
112 
{add_mono_thms: thm list, 

113 
mult_mono_thms: thm list, 

114 
inj_thms: thm list, 

115 
lessD: thm list, 

116 
neqE: thm list, 

117 
simpset: Simplifier.simpset}; 

9420  118 

10691  119 
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

120 
lessD = [], neqE = [], simpset = Simplifier.empty_ss}; 
16458  121 
val extend = I; 
122 
fun merge _ 

123 
({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, 

124 
lessD = lessD1, neqE=neqE1, simpset = simpset1}, 

125 
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, 

126 
lessD = lessD2, neqE=neqE2, simpset = simpset2}) = 

24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

127 
{add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2), 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

128 
mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2), 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

129 
inj_thms = Thm.merge_thms (inj_thms1, inj_thms2), 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

130 
lessD = Thm.merge_thms (lessD1, lessD2), 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

131 
neqE = Thm.merge_thms (neqE1, neqE2), 
10575  132 
simpset = Simplifier.merge_ss (simpset1, simpset2)}; 
22846  133 
); 
9420  134 

135 
val map_data = Data.map; 

24076  136 
val get_data = Data.get o Context.Proof; 
9420  137 

138 

139 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

140 
(*** A fast decision procedure ***) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

141 
(*** Code ported from HOL Light ***) 
6056  142 
(* possible optimizations: 
143 
use (var,coeff) rep or vector rep tp save space; 

144 
treat nonnegative atoms separately rather than adding 0 <= atom 

145 
*) 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

146 

9073  147 
val trace = ref false; 
148 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

149 
datatype lineq_type = Eq  Le  Lt; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

150 

6056  151 
datatype injust = Asm of int 
152 
 Nat of int (* index of atom *) 

6128  153 
 LessD of injust 
154 
 NotLessD of injust 

155 
 NotLeD of injust 

7551
8e934d1a9ac6
Now distinguishes discrete from nondistrete types.
nipkow
parents:
6128
diff
changeset

156 
 NotLeDD of injust 
16358  157 
 Multiplied of IntInf.int * injust 
158 
 Multiplied2 of IntInf.int * injust 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

159 
 Added of injust * injust; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

160 

16358  161 
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

162 

13498  163 
(*  *) 
164 
(* Finding a (counter) example from the trace of a failed elimination *) 

165 
(*  *) 

166 
(* Examples are represented as rational numbers, *) 

167 
(* Dont blame John Harrison for this code  it is entirely mine. TN *) 

168 

169 
exception NoEx; 

170 

14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

171 
(* 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

172 
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

173 
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

174 
*) 
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

175 

22950  176 
fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)] 
177 
 elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)] 

178 
 elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)]; 

13498  179 

180 
(* PRE: ex[v] must be 0! *) 

22950  181 
fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) = 
182 
let 

183 
val rs = map Rat.rat_of_int cs; 

184 
val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero; 

23063  185 
in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end; 
186 
(* 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

187 
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

188 
*) 
13498  189 

22950  190 
fun ratrelmin2 (x as (r, ler), y as (s, les)) = 
23520  191 
case Rat.ord (r, s) 
22950  192 
of EQUAL => (r, (not ler) andalso (not les)) 
193 
 LESS => x 

194 
 GREATER => y; 

195 

196 
fun ratrelmax2 (x as (r, ler), y as (s, les)) = 

23520  197 
case Rat.ord (r, s) 
22950  198 
of EQUAL => (r, ler andalso les) 
199 
 LESS => y 

200 
 GREATER => x; 

13498  201 

14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

202 
val ratrelmin = foldr1 ratrelmin2; 
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

203 
val ratrelmax = foldr1 ratrelmax2; 
13498  204 

22950  205 
fun ratexact up (r, exact) = 
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

206 
if exact then r else 
22950  207 
let 
208 
val (p, q) = Rat.quotient_of_rat r; 

209 
val nth = Rat.inv (Rat.rat_of_int q); 

210 
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

211 

22950  212 
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

213 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

214 
fun choose2 d ((lb, exactl), (ub, exactu)) = 
23520  215 
let val ord = Rat.sign lb in 
22950  216 
if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu) 
217 
then Rat.zero 

218 
else if not d then 

219 
if ord = GREATER 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

220 
then if exactl then lb else ratmiddle (lb, ub) 
22950  221 
else if exactu then ub else ratmiddle (lb, ub) 
222 
else (*discrete domain, both bounds must be exact*) 

23025  223 
if ord = GREATER 
22950  224 
then let val lb' = Rat.roundup lb in 
225 
if Rat.le lb' ub then lb' else raise NoEx end 

226 
else let val ub' = Rat.rounddown ub in 

227 
if Rat.le lb ub' then ub' else raise NoEx end 

228 
end; 

13498  229 

22950  230 
fun findex1 discr (v, lineqs) ex = 
231 
let 

23063  232 
val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs; 
22950  233 
val ineqs = maps elim_eqns nz; 
23063  234 
val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs 
22950  235 
val lb = ratrelmax (map (eval ex v) ge) 
236 
val ub = ratrelmin (map (eval ex v) le) 

21109  237 
in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end; 
13498  238 

239 
fun elim1 v x = 

23063  240 
map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le, 
21109  241 
nth_map v (K Rat.zero) bs)); 
13498  242 

23520  243 
fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs 
23063  244 
of [x] => x =/ nth cs v 
245 
 _ => false; 

13498  246 

247 
(* The base case: 

248 
all variables occur only with positive or only with negative coefficients *) 

249 
fun pick_vars discr (ineqs,ex) = 

23520  250 
let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs 
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

251 
in case nz of [] => ex 
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset

252 
 (_,_,cs) :: _ => 
23520  253 
let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs 
22950  254 
val d = nth discr v; 
23520  255 
val pos = not (Rat.sign (nth cs v) = LESS); 
22950  256 
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

257 
val minmax = 
17951  258 
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

259 
else ratexact true o ratrelmax 
17951  260 
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

261 
else ratexact false o ratrelmin 
23063  262 
val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (nth bs v)), le)) sv 
17951  263 
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

264 
val ineqs' = elim1 v x nz 
21109  265 
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

266 
in pick_vars discr (ineqs',ex') end 
13498  267 
end; 
268 

269 
fun findex0 discr n lineqs = 

22950  270 
let val ineqs = maps elim_eqns lineqs 
271 
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

272 
ineqs 
17951  273 
in pick_vars discr (rineqs,replicate n Rat.zero) end; 
13498  274 

275 
(*  *) 

23197  276 
(* End of counterexample finder. The actual decision procedure starts here. *) 
13498  277 
(*  *) 
278 

5982
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 
(* 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

281 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

282 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

283 
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

284 
 find_add_type(x,Eq) = x 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

285 
 find_add_type(_,Lt) = Lt 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

286 
 find_add_type(Lt,_) = Lt 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

287 
 find_add_type(Le,Le) = Le; 
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 
(* Multiply out an (in)equation. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

291 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

292 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

293 
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

294 
if n = 1 then i 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

295 
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

296 
else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq" 
17524  297 
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

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 
(* Add together (in)equations. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

301 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

302 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

303 
fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 
18330  304 
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

305 
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

306 

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 
(* 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

309 
(* 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

310 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

311 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

312 
fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 
23063  313 
let val c1 = nth l1 v and c2 = nth l2 v 
23261  314 
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

315 
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

316 
val (n1,n2) = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

317 
if (c1 >= 0) = (c2 >= 0) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

318 
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

319 
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

320 
else sys_error "elim_var" 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

321 
else (m1,m2) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

322 
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

323 
then (~n1,~n2) else (n1,n2) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

324 
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

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 
(* The main refutationfinding code. *) 
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 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

330 
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

331 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

332 
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

333 
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

334 

16358  335 
fun calc_blowup (l:IntInf.int list) = 
17496  336 
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

337 
in (length p) * (length n) end; 
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 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

340 
(* Main elimination code: *) 
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 
(* (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

343 
(* *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

344 
(* (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

345 
(* 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

346 
(* *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

347 
(* (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

348 
(* 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

349 
(*  *) 
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 allpairs f xs ys = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

352 
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

353 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

354 
fun extract_first p = 
15531  355 
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

356 
else extract (y::xs) ys 
15531  357 
 extract xs [] = (NONE,xs) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

358 
in extract [] end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

359 

6056  360 
fun print_ineqs ineqs = 
9073  361 
if !trace then 
12262  362 
tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => 
16358  363 
IntInf.toString c ^ 
9073  364 
(case t of Eq => " = "  Lt=> " < "  Le => " <= ") ^ 
16358  365 
commas(map IntInf.toString l)) ineqs)) 
9073  366 
else (); 
6056  367 

13498  368 
type history = (int * lineq list) list; 
369 
datatype result = Success of injust  Failure of history; 

370 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

371 
fun elim (ineqs, hist) = 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

372 
let val dummy = print_ineqs ineqs 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

373 
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

374 
if not (null triv) 
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

375 
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

376 
NONE => elim (nontriv, hist) 
15531  377 
 SOME(Lineq(_,_,_,j)) => Success j 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

378 
else 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

379 
if null nontriv then Failure hist 
13498  380 
else 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

381 
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

382 
if not (null eqs) then 
15570  383 
let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) 
16358  384 
val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y))) 
15570  385 
(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

386 
val c = hd sclist 
15531  387 
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

388 
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

389 
val v = find_index_eq c ceq 
23063  390 
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

391 
(othereqs @ noneqs) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

392 
val others = map (elim_var v eq) roth @ ioth 
13498  393 
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

394 
else 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

395 
let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs 
23063  396 
val numlist = 0 upto (length (hd lists)  1) 
397 
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

398 
val blows = map calc_blowup coeffs 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

399 
val iblows = blows ~~ numlist 
23063  400 
val nziblows = filter_out (fn (i, _) => i = 0) iblows 
13498  401 
in if null nziblows then Failure((~1,nontriv)::hist) 
402 
else 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

403 
let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) 
23063  404 
val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs 
405 
val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes 

13498  406 
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

407 
end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

408 
end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

409 
end; 
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 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

412 
(* Translate back a proof. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

413 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

414 

24076  415 
fun trace_thm msg th = 
416 
(if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th); 

9073  417 

24076  418 
fun trace_term ctxt msg t = 
419 
(if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t) 

420 

421 
fun trace_msg msg = 

422 
if !trace then tracing msg else (); 

9073  423 

13498  424 
(* FIXME OPTIMIZE!!!! (partly done already) 
6056  425 
Addition/Multiplication need i*t representation rather than t+t+... 
10691  426 
Get rid of Mulitplied(2). For Nat LA_Data.number_of should return Suc^n 
427 
because Numerals are not known early enough. 

6056  428 

429 
Simplification may detect a contradiction 'prematurely' due to type 

430 
information: n+1 <= 0 is simplified to False and does not need to be crossed 

431 
with 0 <= n. 

432 
*) 

433 
local 

24076  434 
exception FalseE of thm 
6056  435 
in 
24076  436 
fun mkthm ss asms (just: injust) = 
437 
let 

438 
val ctxt = Simplifier.the_context ss; 

439 
val thy = ProofContext.theory_of ctxt; 

440 
val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; 

441 
val simpset' = Simplifier.inherit_context ss simpset; 

442 
val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) => 

6056  443 
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

444 
([], List.mapPartial (fn thm => if Thm.no_prems thm 
24076  445 
then LA_Data.decomp ctxt (Thm.concl_of thm) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

446 
else NONE) asms) 
6056  447 

10575  448 
fun add2 thm1 thm2 = 
6102  449 
let val conj = thm1 RS (thm2 RS LA_Logic.conjI) 
15531  450 
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

451 
end; 
15531  452 
fun try_add [] _ = NONE 
10575  453 
 try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of 
15531  454 
NONE => try_add thm1s thm2  some => some; 
10575  455 

456 
fun addthms thm1 thm2 = 

457 
case add2 thm1 thm2 of 

15531  458 
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

459 
NONE => ( the (try_add ([thm2] RL inj_thms) thm1) 
15660  460 
handle Option => 
14360  461 
(trace_thm "" thm1; trace_thm "" thm2; 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

462 
sys_error "Lin.arith. failed to add thms") 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

463 
) 
15531  464 
 SOME thm => thm) 
465 
 SOME thm => thm; 

10575  466 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

467 
fun multn(n,thm) = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

468 
let fun mul(i,th) = if i=1 then th else mul(i1, addthms thm th) 
6102  469 
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

470 

15184  471 
fun multn2(n,thm) = 
15531  472 
let val SOME(mth) = 
473 
get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms 

22596  474 
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var; 
15184  475 
val cv = cvar(mth, hd(prems_of mth)); 
24076  476 
val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv))) 
15184  477 
in instantiate ([],[(cv,ct)]) mth end 
10691  478 

6056  479 
fun simp thm = 
17515  480 
let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) 
6102  481 
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end 
6056  482 

24076  483 
fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i) 
484 
 mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i)) 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

485 
 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

486 
 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

487 
 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

488 
 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

489 
 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

490 
 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

491 
 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

492 

9073  493 
in trace_msg "mkthm"; 
12932  494 
let val thm = trace_thm "Final thm:" (mk just) 
17515  495 
in let val fls = simplify simpset' thm 
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

496 
in trace_thm "After simplification:" fls; 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

497 
if LA_Logic.is_False fls then fls 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

498 
else 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

499 
(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

500 
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

501 
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

502 
\Please inform Tobias Nipkow (nipkow@in.tum.de)."; 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

503 
fls) 
12932  504 
end 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

505 
end handle FalseE thm => trace_thm "False reached early:" thm 
12932  506 
end 
6056  507 
end; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

508 

23261  509 
fun coeff poly atom = 
23577  510 
AList.lookup (op aconv) poly atom > the_default (0: integer); 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

511 

23297  512 
fun lcms ks = fold Integer.lcm ks 1; 
10691  513 

514 
fun integ(rlhs,r,rel,rrhs,s,d) = 

17951  515 
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s 
516 
val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs)) 

22846  517 
fun mult(t,r) = 
17951  518 
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

519 
in (t,i * (m div j)) end 
12932  520 
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end 
10691  521 

13498  522 
fun mklineq n atoms = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

523 
fn (item, k) => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

524 
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item 
13498  525 
val lhsa = map (coeff lhs) atoms 
526 
and rhsa = map (coeff rhs) atoms 

18330  527 
val diff = map2 (curry (op )) rhsa lhsa 
13498  528 
val c = ij 
529 
val just = Asm k 

530 
fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j)) 

531 
in case rel of 

532 
"<=" => lineq(c,Le,diff,just) 

533 
 "~<=" => if discrete 

534 
then lineq(1c,Le,map (op ~) diff,NotLeDD(just)) 

535 
else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) 

536 
 "<" => if discrete 

537 
then lineq(c+1,Le,diff,LessD(just)) 

538 
else lineq(c,Lt,diff,just) 

539 
 "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just)) 

540 
 "=" => lineq(c,Eq,diff,just) 

22846  541 
 _ => sys_error("mklineq" ^ rel) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

542 
end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

543 

13498  544 
(*  *) 
545 
(* Print (counter) example *) 

546 
(*  *) 

547 

548 
fun print_atom((a,d),r) = 

17951  549 
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

550 
val s = if d then IntInf.toString p else 
13498  551 
if p = 0 then "0" 
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15922
diff
changeset

552 
else IntInf.toString p ^ "/" ^ IntInf.toString q 
13498  553 
in a ^ " = " ^ s end; 
554 

19049  555 
fun produce_ex sds = 
17496  556 
curry (op ~~) sds 
557 
#> map print_atom 

558 
#> commas 

23197  559 
#> curry (op ^) "Counterexample (possibly spurious):\n"; 
13498  560 

24076  561 
fun trace_ex ctxt params atoms discr n (hist: history) = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

562 
case hist of 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

563 
[] => () 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

564 
 (v, lineqs) :: hist' => 
24076  565 
let 
566 
val frees = map Free params 

567 
fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t)) 

568 
val start = 

569 
if v = ~1 then (hist', findex0 discr n lineqs) 

22950  570 
else (hist, replicate n Rat.zero) 
24076  571 
val ex = SOME (produce_ex (map show_term atoms ~~ discr) 
572 
(uncurry (fold (findex1 discr)) start)) 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

573 
handle NoEx => NONE 
24076  574 
in 
575 
case ex of 

576 
SOME s => (warning "arith failed  see trace for a counterexample"; tracing s) 

577 
 NONE => warning "arith failed" 

578 
end; 

13498  579 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

580 
(*  *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

581 

20268  582 
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

583 
if LA_Logic.is_nat (pTs, atom) 
6056  584 
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

585 
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

586 
else NONE; 
6056  587 

13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

588 
(* This code is tricky. It takes a list of premises in the order they occur 
15531  589 
in the subgoal. Numerical premises are coded as SOME(tuple), nonnumerical 
590 
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

591 
a Lineq. The tricky bit is to convert ~= which is split into two cases < and 
13498  592 
>. 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

593 
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

594 
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

595 
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

596 
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

597 

ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

598 
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

599 
*) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

600 

25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

601 
(* 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

602 
(* 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

603 
(* 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

604 
(* 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

605 
(* 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

606 

24076  607 
fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decompT * int) list) list = 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

608 
let 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

609 
(* 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

610 
(* '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

611 
(* level *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

612 
(* 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

613 
(* 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

614 
(* 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

615 
(* 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

616 
(* 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

617 
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

618 
(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

619 
let 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

620 
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

621 
(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

622 
[[]] 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

623 
 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

624 
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

625 
 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

626 
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

627 
(* [ ?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

628 
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

629 
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

630 
else 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

631 
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

632 
in 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

633 
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

634 
> 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

635 
> List.concat 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

636 
end 
13464  637 

20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

638 
fun number_hyps _ [] = [] 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

639 
 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

640 
 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

641 

d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

642 
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

643 
> (* userdefined preprocessing of the subgoal *) 
24076  644 
(if do_pre then LA_Data.pre_decomp ctxt else Library.single) 
23195  645 
> tap (fn subgoals => trace_msg ("Preprocessing yields " ^ 
646 
string_of_int (length subgoals) ^ " subgoal(s) total.")) 

22846  647 
> (* produce the internal encoding of (in)equalities *) 
24076  648 
map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t)))) 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

649 
> (* splitting of inequalities *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

650 
map (apsnd elim_neq) 
22846  651 
> 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

652 
> (* 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

653 
map (apsnd (number_hyps 0)) 
23195  654 
in 
655 
trace_msg ("Splitting of inequalities yields " ^ 

656 
string_of_int (length result) ^ " subgoal(s) total."); 

657 
result 

658 
end; 

13464  659 

20268  660 
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

661 
(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

662 

20268  663 
fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decompT, _)) : 
664 
(bool * term) list = 

665 
(map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats); 

13498  666 

20268  667 
fun discr (initems : (LA_Data.decompT * int) list) : bool list = 
668 
map fst (Library.foldl add_datoms ([],initems)); 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

669 

24076  670 
fun refutes ctxt params show_ex : 
20268  671 
(typ list * (LA_Data.decompT * int) list) list > injust list > injust list option = 
13498  672 
let 
20268  673 
fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss) 
674 
(js : injust list) : injust list option = 

24076  675 
let 
676 
val atoms = Library.foldl add_atoms ([], initems) 

677 
val n = length atoms 

678 
val mkleq = mklineq n atoms 

679 
val ixs = 0 upto (n  1) 

680 
val iatoms = atoms ~~ ixs 

681 
val natlineqs = List.mapPartial (mknat Ts ixs) iatoms 

682 
val ineqs = map mkleq initems @ natlineqs 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

683 
in case elim (ineqs, []) of 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

684 
Success j => 
24076  685 
(trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); 
20268  686 
refute initemss (js@[j])) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

687 
 Failure hist => 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

688 
(if not show_ex then 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

689 
() 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

690 
else let 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

691 
(* 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

692 
(* 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

693 
(* snd params) as a suffix *) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

694 
val new_count = length Ts  length params  1 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

695 
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

696 
val params' = (new_names @ map fst params) ~~ Ts 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

697 
in 
24076  698 
trace_ex ctxt params' atoms (discr initems) n hist 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

699 
end; NONE) 
13498  700 
end 
15531  701 
 refute [] js = SOME js 
13498  702 
in refute end; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

703 

24076  704 
fun refute ctxt params show_ex do_pre terms : injust list option = 
705 
refutes ctxt params show_ex (split_items ctxt do_pre (map snd params, terms)) []; 

20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

706 

22950  707 
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

708 

24076  709 
fun prove ctxt (params : (string * Term.typ) list) show_ex do_pre Hs concl : injust list option = 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

710 
let 
23190  711 
val _ = trace_msg "prove:" 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

712 
(* 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

713 
(* '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

714 
(* theorem/tactic level *) 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

715 
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

716 
fun is_neq NONE = false 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

717 
 is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") 
24076  718 
val neq_limit = ConfigOption.get ctxt LA_Data.fast_arith_neq_limit; 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

719 
in 
24076  720 
if count is_neq (map (LA_Data.decomp ctxt) Hs') > neq_limit then 
721 
(trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ 

722 
string_of_int neq_limit ^ ")"); NONE) 

723 
else 

724 
refute ctxt params show_ex do_pre Hs' 

23190  725 
end handle TERM ("neg_prop", _) => 
726 
(* since no metalogic negation is available, we can only fail if *) 

727 
(* the conclusion is not of the form 'Trueprop $ _' (simply *) 

728 
(* dropping the conclusion doesn't work either, because even *) 

729 
(* 'False' does not imply arbitrary 'concl::prop') *) 

730 
(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

731 

22846  732 
fun refute_tac ss (i, justs) = 
6074  733 
fn state => 
24076  734 
let 
735 
val ctxt = Simplifier.the_context ss; 

736 
val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ 

737 
string_of_int (length justs) ^ " justification(s)):") state 

738 
val {neqE, ...} = get_data ctxt; 

739 
fun just1 j = 

740 
(* eliminate inequalities *) 

741 
REPEAT_DETERM (eresolve_tac neqE i) THEN 

742 
PRIMITIVE (trace_thm "State after neqE:") THEN 

743 
(* use theorems generated from the actual justifications *) 

744 
METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i 

745 
in 

746 
(* rewrite "[ A1; ...; An ] ==> B" to "[ A1; ...; An; ~B ] ==> False" *) 

747 
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN 

748 
(* userdefined preprocessing of the subgoal *) 

749 
DETERM (LA_Data.pre_tac ctxt i) THEN 

750 
PRIMITIVE (trace_thm "State after pre_tac:") THEN 

751 
(* prove every resulting subgoal, using its justification *) 

752 
EVERY (map just1 justs) 

20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

753 
end state; 
6074  754 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

755 
(* 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

756 
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

757 
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

758 
*) 
24076  759 
fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => 
760 
let 

761 
val ctxt = Simplifier.the_context ss 

762 
val params = rev (Logic.strip_params A) 

763 
val Hs = Logic.strip_assums_hyp A 

764 
val concl = Logic.strip_assums_concl A 

765 
val _ = trace_term ctxt ("Trying to refute subgoal " ^ string_of_int i) A 

766 
in 

767 
case prove ctxt params show_ex true Hs concl of 

768 
NONE => (trace_msg "Refutation failed."; no_tac) 

769 
 SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) 

770 
end); 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

771 

24076  772 
fun cut_lin_arith_tac ss = 
773 
cut_facts_tac (Simplifier.prems_of_ss ss) THEN' 

774 
simpset_lin_arith_tac ss false; 

17613  775 

24076  776 
fun lin_arith_tac ctxt = 
777 
simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); 

778 

779 

5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

780 

13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

781 
(** Forward proof from theorems **) 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

782 

20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

783 
(* 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

784 
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

785 
generated by function split_items. *) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

786 

55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

787 
datatype splittree = Tip of thm list 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

788 
 Spl of thm * cterm * splittree * cterm * splittree; 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

789 

55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

790 
(* "(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

791 

55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

792 
fun extract (imp : cterm) : cterm * cterm = 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

793 
let val (Il, r) = Thm.dest_comb imp 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

794 
val (_, imp1) = Thm.dest_comb Il 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

795 
val (Ict1, _) = Thm.dest_comb imp1 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

796 
val (_, ct1) = Thm.dest_comb Ict1 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

797 
val (Ir, _) = Thm.dest_comb r 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

798 
val (_, Ict2r) = Thm.dest_comb Ir 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

799 
val (Ict2, _) = Thm.dest_comb Ict2r 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

800 
val (_, ct2) = Thm.dest_comb Ict2 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

801 
in (ct1, ct2) end; 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

802 

24076  803 
fun splitasms ctxt (asms : thm list) : splittree = 
804 
let val {neqE, ...} = get_data ctxt 

20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

805 
fun elim_neq (asms', []) = Tip (rev asms') 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

806 
 elim_neq (asms', asm::asms) = 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

807 
(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

808 
SOME spl => 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

809 
let val (ct1, ct2) = extract (cprop_of spl) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

810 
val thm1 = assume ct1 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

811 
val thm2 = assume ct2 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

812 
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

813 
end 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

814 
 NONE => elim_neq (asm::asms', asms)) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

815 
in elim_neq ([], asms) end; 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

816 

24076  817 
fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js) 
818 
 fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js = 

819 
let 

820 
val (thm1, js1) = fwdproof ss tree1 js 

821 
val (thm2, js2) = fwdproof ss tree2 js1 

20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

822 
val thm1' = implies_intr ct1 thm1 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

823 
val thm2' = implies_intr ct2 thm2 
24076  824 
in (thm2' COMP (thm1' COMP thm), js2) end; 
825 
(* FIXME needs handle THM _ => NONE ? *) 

20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

826 

24076  827 
fun prover ss thms Tconcl (js : injust list) pos : thm option = 
828 
let 

829 
val ctxt = Simplifier.the_context ss 

830 
val thy = ProofContext.theory_of ctxt 

831 
val nTconcl = LA_Logic.neg_prop Tconcl 

832 
val cnTconcl = cterm_of thy nTconcl 

833 
val nTconclthm = assume cnTconcl 

834 
val tree = splitasms ctxt (thms @ [nTconclthm]) 

835 
val (Falsethm, _) = fwdproof ss tree js 

836 
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI 

837 
val concl = implies_intr cnTconcl Falsethm COMP contr 

838 
in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end 

839 
(*in case concl contains ?var, which makes assume fail:*) (* FIXME Variable.import_terms *) 

840 
handle THM _ => NONE; 

13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

841 

ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

842 
(* PRE: concl is not negated! 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

843 
This assumption is OK because 
24076  844 
1. lin_arith_simproc tries both to prove and disprove concl and 
845 
2. lin_arith_simproc is applied by the Simplifier which 

13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

846 
dives into terms and will thus try the nonnegated concl anyway. 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

847 
*) 
24076  848 
fun lin_arith_simproc ss concl = 
849 
let 

850 
val ctxt = Simplifier.the_context ss 

851 
val thms = List.concat (map LA_Logic.atomize (Simplifier.prems_of_ss ss)) 

852 
val Hs = map Thm.prop_of thms 

6102  853 
val Tconcl = LA_Logic.mk_Trueprop concl 
24076  854 
in 
855 
case prove ctxt [] false false Hs Tconcl of (* concl provable? *) 

856 
SOME js => prover ss thms Tconcl js true 

857 
 NONE => 

858 
let val nTconcl = LA_Logic.neg_prop Tconcl in 

859 
case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *) 

860 
SOME js => prover ss thms nTconcl js false 

861 
 NONE => NONE 

862 
end 

863 
end; 

6074  864 

865 
end; 