author  wenzelm 
Mon, 16 Feb 2009 21:23:33 +0100  
changeset 29758  7a3b5bbed313 
parent 27020  b5b8afc9fdcd 
child 30406  15dc25f8a0e2 
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 

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

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

15 

6102  16 
signature LIN_ARITH_LOGIC = 
17 
sig 

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

18 
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

19 
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

20 
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

21 
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

22 
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

23 
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

24 
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

25 
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

26 
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

27 
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

28 
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

29 
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

30 
val mk_nat_thm : theory > term > thm 
6102  31 
end; 
32 
(* 

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

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

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

36 

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

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

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

41 
the form 'Trueprop $ _' 

6128  42 

43 
is_nat(parametertypes,t) = t:nat 

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

6102  45 
*) 
46 

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

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

48 
sig 
24076  49 
(*internal representation of linear (in)equations:*) 
26945  50 
type decomp = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool 
51 
val decomp: Proof.context > term > decomp option 

24076  52 
val domain_is_nat: term > bool 
53 

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

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

56 

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

58 
val pre_tac: Proof.context > int > tactic 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

59 
val number_of: int * typ > term 
24076  60 

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

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

24112  63 
val fast_arith_neq_limit: int Config.T 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

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

66 
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

67 
where Rel is one of "<", "~<", "<=", "~<=" and "=" and 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

68 
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

69 
(y, respectively) into a list of summand * multiplicity 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

70 
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

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

72 

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

73 
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

74 

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

75 
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

76 
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

77 
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

78 
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

79 
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

80 
insensitive to them.) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

81 

9420  82 
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

83 
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

84 
otherwise <= can grow to massive proportions. 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

86 

6062  87 
signature FAST_LIN_ARITH = 
88 
sig 

15184  89 
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

90 
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} 
15184  91 
> {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}) 
24076  93 
> Context.generic > Context.generic 
19314  94 
val trace: bool ref 
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

95 
val warning_count: int ref; 
17613  96 
val cut_lin_arith_tac: simpset > int > tactic 
24076  97 
val lin_arith_tac: Proof.context > bool > int > tactic 
98 
val lin_arith_simproc: simpset > term > thm option 

6062  99 
end; 
100 

24076  101 
functor Fast_Lin_Arith 
102 
(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

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

104 

9420  105 

106 
(** theory data **) 

107 

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

112 
mult_mono_thms: thm list, 

113 
inj_thms: thm list, 

114 
lessD: thm list, 

115 
neqE: thm list, 

116 
simpset: Simplifier.simpset}; 

9420  117 

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

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

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

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

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

125 
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

126 
{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

127 
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

128 
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

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

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

134 
val map_data = Data.map; 

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

137 

138 

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

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

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

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

144 
*) 

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

145 

9073  146 
val trace = ref false; 
147 

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

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

149 

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

6128  152 
 LessD of injust 
153 
 NotLessD of injust 

154 
 NotLeD of injust 

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

155 
 NotLeDD of injust 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

156 
 Multiplied of int * injust 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

157 
 Multiplied2 of int * injust 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

159 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

160 
datatype lineq = Lineq of int * lineq_type * int list * injust; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

161 

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

164 
(*  *) 

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

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

167 

168 
exception NoEx; 

169 

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

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

171 
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

172 
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

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

174 

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

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

13498  178 

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

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

180 
fun eval ex v (a, le, cs) = 
22950  181 
let 
182 
val rs = map Rat.rat_of_int cs; 

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

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

186 
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

187 
*) 
13498  188 

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

193 
 GREATER => y; 

194 

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

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

199 
 GREATER => x; 

13498  200 

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

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

202 
val ratrelmax = foldr1 ratrelmax2; 
13498  203 

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

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

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

209 
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

210 

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

212 

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

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

217 
else if not d then 

218 
if ord = GREATER 

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

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

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

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

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

227 
end; 

13498  228 

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

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

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

238 
fun elim1 v x = 

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

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

13498  245 

246 
(* The base case: 

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

248 
fun pick_vars discr (ineqs,ex) = 

23520  249 
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

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

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

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

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

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

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

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

268 
fun findex0 discr n lineqs = 

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

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

274 
(*  *) 

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

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

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

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

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

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

284 
 find_add_type(_,Lt) = Lt 
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(Le,Le) = Le; 
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 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

289 
(* Multiply out an (in)equation. *) 
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 

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

292 
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

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

294 
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

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

297 

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

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

304 
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

305 

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

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

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

314 
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

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

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

317 
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

318 
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

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

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

321 
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

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

323 
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

324 

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

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

329 
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

330 

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

331 
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

332 
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

333 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

334 
fun calc_blowup l = 
17496  335 
let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l) 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

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

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

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

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

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

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

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

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

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

348 
(*  *) 
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 
fun allpairs f xs ys = 
26945  351 
maps (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

352 

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

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

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

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

358 

6056  359 
fun print_ineqs ineqs = 
9073  360 
if !trace then 
12262  361 
tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

362 
string_of_int c ^ 
9073  363 
(case t of Eq => " = "  Lt=> " < "  Le => " <= ") ^ 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

364 
commas(map string_of_int l)) ineqs)) 
9073  365 
else (); 
6056  366 

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

369 

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

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

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

372 
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

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

374 
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

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

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

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

380 
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

381 
if not (null eqs) then 
15570  382 
let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

383 
val sclist = sort (fn (x,y) => int_ord (abs x, abs y)) 
15570  384 
(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

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

387 
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

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

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

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

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

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

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

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

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

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

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

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

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 
(* Translate back a proof. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

413 

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

9073  416 

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

420 
fun trace_msg msg = 

421 
if !trace then tracing msg else (); 

9073  422 

27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

423 
val warning_count = ref 0; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

424 
val warning_count_max = 10; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

425 

26835
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

426 
val union_term = curry (gen_union Pattern.aeconv); 
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

427 
val union_bterm = curry (gen_union 
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

428 
(fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'))); 
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

429 

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

6056  434 

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

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

437 
with 0 <= n. 

438 
*) 

439 
local 

24076  440 
exception FalseE of thm 
6056  441 
in 
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

442 

24076  443 
fun mkthm ss asms (just: injust) = 
444 
let 

445 
val ctxt = Simplifier.the_context ss; 

446 
val thy = ProofContext.theory_of ctxt; 

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

448 
val simpset' = Simplifier.inherit_context ss simpset; 

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

26835
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

450 
union_term (map fst lhs) (union_term (map fst rhs) ats)) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

451 
([], List.mapPartial (fn thm => if Thm.no_prems thm 
24076  452 
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

453 
else NONE) asms) 
6056  454 

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

458 
end; 
15531  459 
fun try_add [] _ = NONE 
10575  460 
 try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of 
15531  461 
NONE => try_add thm1s thm2  some => some; 
10575  462 

463 
fun addthms thm1 thm2 = 

464 
case add2 thm1 thm2 of 

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

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

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

470 
) 
15531  471 
 SOME thm => thm) 
472 
 SOME thm => thm; 

10575  473 

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

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

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

477 

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

22596  481 
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var; 
15184  482 
val cv = cvar(mth, hd(prems_of mth)); 
24076  483 
val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv))) 
15184  484 
in instantiate ([],[(cv,ct)]) mth end 
10691  485 

6056  486 
fun simp thm = 
17515  487 
let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) 
6102  488 
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end 
6056  489 

24076  490 
fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i) 
491 
 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

492 
 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

493 
 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

494 
 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

495 
 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

496 
 mk (Added (j1, j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

497 
 mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j))) 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

498 
 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

499 

27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

500 
in 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

501 
let 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

502 
val _ = trace_msg "mkthm"; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

503 
val thm = trace_thm "Final thm:" (mk just); 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

504 
val fls = simplify simpset' thm; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

505 
val _ = trace_thm "After simplification:" fls; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

506 
val _ = 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

507 
if LA_Logic.is_False fls then () 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

508 
else 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

509 
let val count = CRITICAL (fn () => inc warning_count) in 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

510 
if count > warning_count_max then () 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

511 
else 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

512 
(tracing (cat_lines 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

513 
(["Assumptions:"] @ map Display.string_of_thm asms @ [""] @ 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

514 
["Proved:", Display.string_of_thm fls, ""] @ 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

515 
(if count <> warning_count_max then [] 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

516 
else ["\n(Reached maximal message count  disabling future warnings)"]))); 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

517 
warning "Linear arithmetic should have refuted the assumptions.\n\ 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

518 
\Please inform Tobias Nipkow (nipkow@in.tum.de).") 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

519 
end; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

520 
in fls end 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

521 
handle FalseE thm => trace_thm "False reached early:" thm 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

522 
end; 
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

523 

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

525 

23261  526 
fun coeff poly atom = 
26835
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

527 
AList.lookup Pattern.aeconv poly atom > the_default 0; 
10691  528 

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

17951  530 
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

531 
val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs)) 
22846  532 
fun mult(t,r) = 
17951  533 
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

534 
in (t,i * (m div j)) end 
12932  535 
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end 
10691  536 

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

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

539 
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item 
13498  540 
val lhsa = map (coeff lhs) atoms 
541 
and rhsa = map (coeff rhs) atoms 

18330  542 
val diff = map2 (curry (op )) rhsa lhsa 
13498  543 
val c = ij 
544 
val just = Asm k 

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

546 
in case rel of 

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

548 
 "~<=" => if discrete 

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

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

551 
 "<" => if discrete 

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

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

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

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

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

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

558 

13498  559 
(*  *) 
560 
(* Print (counter) example *) 

561 
(*  *) 

562 

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

17951  564 
let val (p,q) = Rat.quotient_of_rat r 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

565 
val s = if d then string_of_int p else 
13498  566 
if p = 0 then "0" 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

567 
else string_of_int p ^ "/" ^ string_of_int q 
13498  568 
in a ^ " = " ^ s end; 
569 

19049  570 
fun produce_ex sds = 
17496  571 
curry (op ~~) sds 
572 
#> map print_atom 

573 
#> commas 

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

24076  576 
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

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

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

579 
 (v, lineqs) :: hist' => 
24076  580 
let 
581 
val frees = map Free params 

24920  582 
fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t)) 
24076  583 
val start = 
584 
if v = ~1 then (hist', findex0 discr n lineqs) 

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

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

588 
handle NoEx => NONE 
24076  589 
in 
590 
case ex of 

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

592 
 NONE => warning "arith failed" 

593 
end; 

13498  594 

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

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

596 

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

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

600 
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

601 
else NONE; 
6056  602 

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

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

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

608 
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

609 
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

610 
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

611 
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

612 

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

613 
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

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

615 

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

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

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

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

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

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

621 

26945  622 
fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decomp * 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

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

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

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

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

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

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

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

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

631 
(* can be applied, and split the premise accordingly. *) 
26945  632 
fun elim_neq (ineqs : (LA_Data.decomp option * bool) list) : 
633 
(LA_Data.decomp option * bool) list list = 

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

634 
let 
26945  635 
fun elim_neq' nat_only ([] : (LA_Data.decomp option * bool) list) : 
636 
(LA_Data.decomp option * bool) list list = 

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

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

638 
 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

639 
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

640 
 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

641 
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

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

643 
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

644 
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

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

646 
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

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

648 
ineqs > elim_neq' true 
26945  649 
> maps (elim_neq' false) 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

650 
end 
13464  651 

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

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

653 
 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

654 
 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

655 

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

656 
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

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

22846  661 
> (* produce the internal encoding of (in)equalities *) 
24076  662 
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

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

664 
map (apsnd elim_neq) 
22846  665 
> 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

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

667 
map (apsnd (number_hyps 0)) 
23195  668 
in 
669 
trace_msg ("Splitting of inequalities yields " ^ 

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

671 
result 

672 
end; 

13464  673 

26945  674 
fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decomp, _)) : term list = 
26835
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

675 
union_term (map fst lhs) (union_term (map fst rhs) ats); 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

676 

26945  677 
fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) : 
20268  678 
(bool * term) list = 
26835
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset

679 
union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); 
13498  680 

26945  681 
fun discr (initems : (LA_Data.decomp * int) list) : bool list = 
20268  682 
map fst (Library.foldl add_datoms ([],initems)); 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

683 

24076  684 
fun refutes ctxt params show_ex : 
26945  685 
(typ list * (LA_Data.decomp * int) list) list > injust list > injust list option = 
686 
let 

687 
fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) = 

688 
let 

689 
val atoms = Library.foldl add_atoms ([], initems) 

690 
val n = length atoms 

691 
val mkleq = mklineq n atoms 

692 
val ixs = 0 upto (n  1) 

693 
val iatoms = atoms ~~ ixs 

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

695 
val ineqs = map mkleq initems @ natlineqs 

696 
in case elim (ineqs, []) of 

697 
Success j => 

698 
(trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); 

699 
refute initemss (js @ [j])) 

700 
 Failure hist => 

701 
(if not show_ex then () 

702 
else 

703 
let 

704 
val (param_names, ctxt') = ctxt > Variable.variant_fixes (map fst params) 

705 
val (more_names, ctxt'') = ctxt' > Variable.variant_fixes 

706 
(Name.invents (Variable.names_of ctxt') Name.uu (length Ts  length params)) 

707 
val params' = (more_names @ param_names) ~~ Ts 

708 
in 

709 
trace_ex ctxt'' params' atoms (discr initems) n hist 

710 
end; NONE) 

711 
end 

712 
 refute [] js = SOME js 

713 
in refute end; 

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

714 

24076  715 
fun refute ctxt params show_ex do_pre terms : injust list option = 
716 
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

717 

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

719 

26945  720 
fun prove ctxt params 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

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

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

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

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

726 
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

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

728 
 is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") 
24112  729 
val neq_limit = Config.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

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

733 
string_of_int neq_limit ^ ")"); NONE) 

734 
else 

735 
refute ctxt params show_ex do_pre Hs' 

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

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

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

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

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

742 

22846  743 
fun refute_tac ss (i, justs) = 
6074  744 
fn state => 
24076  745 
let 
746 
val ctxt = Simplifier.the_context ss; 

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

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

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

750 
fun just1 j = 

751 
(* eliminate inequalities *) 

752 
REPEAT_DETERM (eresolve_tac neqE i) THEN 

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

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

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

756 
in 

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

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

759 
(* userdefined preprocessing of the subgoal *) 

760 
DETERM (LA_Data.pre_tac ctxt i) THEN 

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

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

763 
EVERY (map just1 justs) 

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

764 
end state; 
6074  765 

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

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

767 
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

768 
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

769 
*) 
24076  770 
fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => 
771 
let 

772 
val ctxt = Simplifier.the_context ss 

773 
val params = rev (Logic.strip_params A) 

774 
val Hs = Logic.strip_assums_hyp A 

775 
val concl = Logic.strip_assums_concl A 

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

777 
in 

778 
case prove ctxt params show_ex true Hs concl of 

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

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

781 
end); 

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

782 

24076  783 
fun cut_lin_arith_tac ss = 
784 
cut_facts_tac (Simplifier.prems_of_ss ss) THEN' 

785 
simpset_lin_arith_tac ss false; 

17613  786 

24076  787 
fun lin_arith_tac ctxt = 
788 
simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); 

789 

790 

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

791 

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

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

793 

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

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

795 
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

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

797 

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

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

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

800 

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

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

802 

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

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

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

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

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

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

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

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

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

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

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

813 

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

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

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

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

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

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

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

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

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

823 
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

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

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

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

827 

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

830 
let 

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

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

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

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

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

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

837 

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

840 
val ctxt = Simplifier.the_context ss 

841 
val thy = ProofContext.theory_of ctxt 

842 
val nTconcl = LA_Logic.neg_prop Tconcl 

843 
val cnTconcl = cterm_of thy nTconcl 

844 
val nTconclthm = assume cnTconcl 

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

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

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

848 
val concl = implies_intr cnTconcl Falsethm COMP contr 

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

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

851 
handle THM _ => NONE; 

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

852 

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

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

854 
This assumption is OK because 
24076  855 
1. lin_arith_simproc tries both to prove and disprove concl and 
856 
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

857 
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

858 
*) 
24076  859 
fun lin_arith_simproc ss concl = 
860 
let 

861 
val ctxt = Simplifier.the_context ss 

26945  862 
val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss) 
24076  863 
val Hs = map Thm.prop_of thms 
6102  864 
val Tconcl = LA_Logic.mk_Trueprop concl 
24076  865 
in 
866 
case prove ctxt [] false false Hs Tconcl of (* concl provable? *) 

867 
SOME js => prover ss thms Tconcl js true 

868 
 NONE => 

869 
let val nTconcl = LA_Logic.neg_prop Tconcl in 

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

871 
SOME js => prover ss thms nTconcl js false 

872 
 NONE => NONE 

873 
end 

874 
end; 

6074  875 

876 
end; 