author  haftmann 
Mon, 21 May 2007 19:11:42 +0200  
changeset 23063  b4ee6ec4f9c6 
parent 23025  7507f94adc32 
child 23190  d45c4d6c5f15 
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$ 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

3 
Author: Tobias Nipkow 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

4 
Copyright 1998 TU Munich 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

5 

6062  6 
A generic linear arithmetic package. 
6102  7 
It provides two tactics 
8 

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

9 
lin_arith_tac: int > tactic 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

10 
cut_lin_arith_tac: thms > int > tactic 
6102  11 

12 
and a simplification procedure 

13 

16458  14 
lin_arith_prover: theory > simpset > term > thm option 
6102  15 

16 
Only take premises and conclusions into account that are already (negated) 

17 
(in)equations. lin_arith_prover tries to prove or disprove the term. 

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

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

19 

9073  20 
(* Debugging: set Fast_Arith.trace *) 
7582  21 

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

22 
(*** Data needed for setting up the linear arithmetic package ***) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

23 

6102  24 
signature LIN_ARITH_LOGIC = 
25 
sig 

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

26 
val conjI : thm (* P ==> Q ==> P & Q *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

27 
val ccontr : thm (* (~ P ==> False) ==> P *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

28 
val notI : thm (* (P ==> False) ==> ~ P *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

29 
val not_lessD : thm (* ~(m < n) ==> n <= m *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

30 
val not_leD : thm (* ~(m <= n) ==> n < m *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

31 
val sym : thm (* x = y ==> y = x *) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

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

33 
val atomize : thm > thm list 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

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

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

36 
val is_False : thm > bool 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

37 
val is_nat : typ list * term > bool 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

38 
val mk_nat_thm : theory > term > thm 
6102  39 
end; 
40 
(* 

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

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

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

44 

19318  45 
neg_prop(t) = neg if t is wrapped up in Trueprop and 
46 
neg is the (logically) negated version of t, where the negation 

6102  47 
of a negative term is the term itself (no double negation!); 
6128  48 

49 
is_nat(parametertypes,t) = t:nat 

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

6102  51 
*) 
52 

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

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

54 
sig 
20268  55 
(* internal representation of linear (in)equations: *) 
56 
type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool 

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

57 
val decomp: theory > term > decompT option 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

58 
val domain_is_nat : term > bool 
20268  59 
(* preprocessing, performed on a representation of subgoals as list of premises: *) 
60 
val pre_decomp: theory > typ list * term list > (typ list * term list) list 

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

62 
val pre_tac : int > Tactical.tactic 

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

63 
val number_of : IntInf.int * typ > term 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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}) 
10575  93 
> theory > theory 
19314  94 
val trace: bool ref 
14510  95 
val fast_arith_neq_limit: int ref 
16458  96 
val lin_arith_prover: theory > simpset > term > thm option 
17892  97 
val lin_arith_tac: bool > int > tactic 
17613  98 
val cut_lin_arith_tac: simpset > int > tactic 
6062  99 
end; 
100 

22846  101 
functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC 
6102  102 
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 

16458  108 
structure Data = TheoryDataFun 
22846  109 
( 
15184  110 
type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, 
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset

111 
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}; 
9420  112 

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

114 
lessD = [], neqE = [], simpset = Simplifier.empty_ss}; 
9420  115 
val copy = I; 
16458  116 
val extend = I; 
9420  117 

16458  118 
fun merge _ 
119 
({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, 

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

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

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

9420  123 
{add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), 
15184  124 
mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2), 
10575  125 
inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), 
126 
lessD = Drule.merge_rules (lessD1, lessD2), 

15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset

127 
neqE = Drule.merge_rules (neqE1, neqE2), 
10575  128 
simpset = Simplifier.merge_ss (simpset1, simpset2)}; 
22846  129 
); 
9420  130 

131 
val map_data = Data.map; 

132 

133 

134 

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

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

136 
(*** Code ported from HOL Light ***) 
6056  137 
(* possible optimizations: 
138 
use (var,coeff) rep or vector rep tp save space; 

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

140 
*) 

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

141 

9073  142 
val trace = ref false; 
143 

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

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

145 

6056  146 
datatype injust = Asm of int 
147 
 Nat of int (* index of atom *) 

6128  148 
 LessD of injust 
149 
 NotLessD of injust 

150 
 NotLeD of injust 

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

151 
 NotLeDD of injust 
16358  152 
 Multiplied of IntInf.int * injust 
153 
 Multiplied2 of IntInf.int * injust 

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

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

155 

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

157 

13498  158 
(*  *) 
159 
(* Finding a (counter) example from the trace of a failed elimination *) 

160 
(*  *) 

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

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

163 

164 
exception NoEx; 

165 

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

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

167 
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

168 
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

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

170 

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

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

13498  174 

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

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

178 
val rs = map Rat.rat_of_int cs; 

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

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

182 
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

183 
*) 
13498  184 

22950  185 
fun ratrelmin2 (x as (r, ler), y as (s, les)) = 
186 
case Rat.cmp (r, s) 

187 
of EQUAL => (r, (not ler) andalso (not les)) 

188 
 LESS => x 

189 
 GREATER => y; 

190 

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

192 
case Rat.cmp (r, s) 

193 
of EQUAL => (r, ler andalso les) 

194 
 LESS => y 

195 
 GREATER => x; 

13498  196 

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

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

198 
val ratrelmax = foldr1 ratrelmax2; 
13498  199 

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

201 
if exact then r else 
22950  202 
let 
203 
val (p, q) = Rat.quotient_of_rat r; 

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

205 
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

206 

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

208 

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

209 
fun choose2 d ((lb, exactl), (ub, exactu)) = 
22950  210 
let val ord = Rat.cmp_zero lb in 
211 
if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu) 

212 
then Rat.zero 

213 
else if not d then 

214 
if ord = GREATER 

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

215 
then if exactl then lb else ratmiddle (lb, ub) 
22950  216 
else if exactu then ub else ratmiddle (lb, ub) 
217 
else (*discrete domain, both bounds must be exact*) 

23025  218 
if ord = GREATER 
22950  219 
then let val lb' = Rat.roundup lb in 
220 
if Rat.le lb' ub then lb' else raise NoEx end 

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

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

223 
end; 

13498  224 

22950  225 
fun findex1 discr (v, lineqs) ex = 
226 
let 

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

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

234 
fun elim1 v x = 

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

23063  238 
fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs 
239 
of [x] => x =/ nth cs v 

240 
 _ => false; 

13498  241 

242 
(* The base case: 

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

244 
fun pick_vars discr (ineqs,ex) = 

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

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

247 
 (_,_,cs) :: _ => 
22950  248 
let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs 
249 
val d = nth discr v; 

23063  250 
val pos = not (Rat.cmp_zero (nth cs v) = LESS); 
22950  251 
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

252 
val minmax = 
17951  253 
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

254 
else ratexact true o ratrelmax 
17951  255 
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

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

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

261 
in pick_vars discr (ineqs',ex') end 
13498  262 
end; 
263 

264 
fun findex0 discr n lineqs = 

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

267 
ineqs 
17951  268 
in pick_vars discr (rineqs,replicate n Rat.zero) end; 
13498  269 

270 
(*  *) 

271 
(* End of counter example finder. The actual decision procedure starts here. *) 

272 
(*  *) 

273 

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

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

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

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

277 

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

278 
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

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

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

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

282 
 find_add_type(Le,Le) = Le; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

283 

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

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

285 
(* Multiply out an (in)equation. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

287 

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

288 
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

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

290 
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

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

293 

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

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

295 
(* Add together (in)equations. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

297 

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

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

300 
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

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

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

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 
fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 
23063  308 
let val c1 = nth l1 v and c2 = nth l2 v 
16358  309 
val m = lcm(abs c1, abs c2) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

310 
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

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

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

313 
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

314 
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

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

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

317 
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

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

319 
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

320 

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

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

322 
(* The main refutationfinding code. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

324 

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

325 
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

326 

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

327 
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

328 
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

329 

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

332 
in (length p) * (length n) end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

333 

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

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

335 
(* Main elimination code: *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

347 
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

348 

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

349 
fun extract_first p = 
15531  350 
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

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

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

354 

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

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

365 

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

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

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

368 
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

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

370 
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

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

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

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

376 
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

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

381 
val c = hd sclist 
15531  382 
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

383 
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

384 
val v = find_index_eq c ceq 
23063  385 
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

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

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

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

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

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

394 
val iblows = blows ~~ numlist 
23063  395 
val nziblows = filter_out (fn (i, _) => i = 0) iblows 
13498  396 
in if null nziblows then Failure((~1,nontriv)::hist) 
397 
else 

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

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

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

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

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

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

405 

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

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

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

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

409 

20268  410 
fun trace_thm (msg : string) (th : thm) : thm = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

411 
(if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th); 
9073  412 

20268  413 
fun trace_msg (msg : string) : unit = 
12262  414 
if !trace then tracing msg else (); 
9073  415 

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

6056  420 

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

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

423 
with 0 <= n. 

424 
*) 

425 
local 

426 
exception FalseE of thm 

427 
in 

22846  428 
fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm = 
15922
7ef183f3fc98
neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow
parents:
15660
diff
changeset

429 
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = 
16458  430 
Data.get sg; 
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
17613
diff
changeset

431 
val simpset' = Simplifier.inherit_context ss simpset; 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

432 
val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) => 
6056  433 
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

434 
([], List.mapPartial (fn thm => if Thm.no_prems thm 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

435 
then LA_Data.decomp sg (concl_of thm) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

436 
else NONE) asms) 
6056  437 

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

441 
end; 
15531  442 
fun try_add [] _ = NONE 
10575  443 
 try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of 
15531  444 
NONE => try_add thm1s thm2  some => some; 
10575  445 

446 
fun addthms thm1 thm2 = 

447 
case add2 thm1 thm2 of 

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

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

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

453 
) 
15531  454 
 SOME thm => thm) 
455 
 SOME thm => thm; 

10575  456 

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

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

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

460 

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

22596  464 
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var; 
15184  465 
val cv = cvar(mth, hd(prems_of mth)); 
466 
val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv))) 

467 
in instantiate ([],[(cv,ct)]) mth end 

10691  468 

6056  469 
fun simp thm = 
17515  470 
let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) 
6102  471 
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end 
6056  472 

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

473 
fun mk (Asm i) = trace_thm ("Asm " ^ Int.toString i) (nth asms i) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

474 
 mk (Nat i) = trace_thm ("Nat " ^ Int.toString i) (LA_Logic.mk_nat_thm sg (nth atoms i)) 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

475 
 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

476 
 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

477 
 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

478 
 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

479 
 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

480 
 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

481 
 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

482 

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

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

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

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

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

490 
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

491 
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

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

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

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

498 

16358  499 
fun coeff poly atom : IntInf.int = 
17325  500 
AList.lookup (op =) poly atom > the_default 0; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

501 

20280
ad9fbbd01535
type annotations fixed (IntInf.int, to make SML/NJ happy)
webertj
parents:
20276
diff
changeset

502 
fun lcms (is : IntInf.int list) : IntInf.int = Library.foldl lcm (1, is); 
10691  503 

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

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

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

509 
in (t,i * (m div j)) end 
12932  510 
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end 
10691  511 

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

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

514 
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item 
13498  515 
val lhsa = map (coeff lhs) atoms 
516 
and rhsa = map (coeff rhs) atoms 

18330  517 
val diff = map2 (curry (op )) rhsa lhsa 
13498  518 
val c = ij 
519 
val just = Asm k 

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

521 
in case rel of 

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

523 
 "~<=" => if discrete 

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

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

526 
 "<" => if discrete 

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

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

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

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

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

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

533 

13498  534 
(*  *) 
535 
(* Print (counter) example *) 

536 
(*  *) 

537 

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

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

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

542 
else IntInf.toString p ^ "/" ^ IntInf.toString q 
13498  543 
in a ^ " = " ^ s end; 
544 

19049  545 
fun produce_ex sds = 
17496  546 
curry (op ~~) sds 
547 
#> map print_atom 

548 
#> commas 

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

549 
#> curry (op ^) "Counter example (possibly spurious):\n"; 
13498  550 

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

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

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

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

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

555 
let val frees = map Free params 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

556 
fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t)) 
22950  557 
val start = if v = ~1 then (hist', findex0 discr n lineqs) 
558 
else (hist, replicate n Rat.zero) 

559 
val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) 

560 
(uncurry (fold (findex1 discr)) start)) 

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

561 
handle NoEx => NONE 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

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

564 
SOME s => (warning "arith failed  see trace for a counter example"; tracing s) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

565 
 NONE => warning "arith failed" 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

566 
end; 
13498  567 

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

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

569 

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

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

573 
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

574 
else NONE; 
6056  575 

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

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

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

581 
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

582 
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

583 
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

584 
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

585 

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

586 
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

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

588 

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

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

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

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

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

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

594 

22846  595 
fun split_items sg (do_pre : bool) (Ts, terms) : 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

596 
(typ list * (LA_Data.decompT * int) list) list = 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

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

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

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

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

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

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

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

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

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

606 
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

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

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

609 
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

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

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

612 
 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

613 
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

614 
 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

615 
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

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

617 
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

618 
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

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

620 
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

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

622 
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

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

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

625 
end 
13464  626 

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

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

628 
 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

629 
 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

630 

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

631 
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

632 
> (* userdefined preprocessing of the subgoal *) 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

633 
(if do_pre then LA_Data.pre_decomp sg else Library.single) 
22846  634 
> (* produce the internal encoding of (in)equalities *) 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

635 
map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t)))) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

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

637 
map (apsnd elim_neq) 
22846  638 
> 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

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

640 
map (apsnd (number_hyps 0)) 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

641 
in result end; 
13464  642 

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

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

645 

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

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

13498  649 

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

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

652 

20268  653 
fun refutes (sg : theory) (params : (string * typ) list) (show_ex : bool) : 
654 
(typ list * (LA_Data.decompT * int) list) list > injust list > injust list option = 

13498  655 
let 
20268  656 
fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss) 
657 
(js : injust list) : injust list option = 

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

658 
let val atoms = Library.foldl add_atoms ([], initems) 
13498  659 
val n = length atoms 
660 
val mkleq = mklineq n atoms 

661 
val ixs = 0 upto (n1) 

662 
val iatoms = atoms ~~ ixs 

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

663 
val natlineqs = List.mapPartial (mknat Ts ixs) iatoms 
13498  664 
val ineqs = map mkleq initems @ natlineqs 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

666 
Success j => 
20268  667 
(trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); 
668 
refute initemss (js@[j])) 

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

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

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

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

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

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

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

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

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

677 
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

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

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

680 
trace_ex (sg, params', atoms, discr initems, n, hist) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

681 
end; NONE) 
13498  682 
end 
15531  683 
 refute [] js = SOME js 
13498  684 
in refute end; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

685 

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

686 
fun refute (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

687 
(do_pre : bool) (terms : term list) : injust list option = 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

688 
refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) []; 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

689 

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

691 

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

692 
(* The limit on the number of ~= allowed. 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

693 
Because each ~= is split into two cases, this can lead to an explosion. 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

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

695 
val fast_arith_neq_limit = ref 9; 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

696 

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

697 
fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

698 
(do_pre : bool) (Hs : term list) (concl : term) : injust list option = 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

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

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

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

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

703 
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

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

705 
 is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

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

707 
trace_msg "prove"; 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

708 
if count is_neq (map (LA_Data.decomp sg) Hs') 
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

709 
> !fast_arith_neq_limit then ( 
20268  710 
trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ 
711 
string_of_int (!fast_arith_neq_limit) ^ ")"); 

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

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

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

714 
refute sg params show_ex do_pre Hs' 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

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

716 

22846  717 
fun refute_tac ss (i, justs) = 
6074  718 
fn state => 
20268  719 
let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ 
720 
Int.toString (length justs) ^ " justification(s)):") state 

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

721 
val sg = theory_of_thm state 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

722 
val {neqE, ...} = Data.get sg 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

723 
fun just1 j = 
20268  724 
(* eliminate inequalities *) 
725 
REPEAT_DETERM (eresolve_tac neqE i) THEN 

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

726 
PRIMITIVE (trace_thm "State after neqE:") THEN 
20268  727 
(* use theorems generated from the actual justifications *) 
728 
METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i 

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

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

731 
(* userdefined preprocessing of the subgoal *) 

732 
DETERM (LA_Data.pre_tac i) THEN 

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

733 
PRIMITIVE (trace_thm "State after pre_tac:") THEN 
20268  734 
(* prove every resulting subgoal, using its justification *) 
735 
EVERY (map just1 justs) 

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

736 
end state; 
6074  737 

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

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

739 
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

740 
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

741 
*) 
20268  742 
fun simpset_lin_arith_tac (ss : simpset) (show_ex : bool) (i : int) (st : thm) = 
743 
SUBGOAL (fn (A,_) => 

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

744 
let val params = rev (Logic.strip_params A) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

745 
val Hs = Logic.strip_assums_hyp A 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

746 
val concl = Logic.strip_assums_concl A 
12932  747 
in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st; 
22578  748 
case prove (Thm.theory_of_thm st) params show_ex true Hs concl of 
15531  749 
NONE => (trace_msg "Refutation failed."; no_tac) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

750 
 SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) 
9420  751 
end) i st; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

752 

20268  753 
fun lin_arith_tac (show_ex : bool) (i : int) (st : thm) = 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

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

755 
(Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

756 
show_ex i st; 
17613  757 

20268  758 
fun cut_lin_arith_tac (ss : simpset) (i : int) = 
17613  759 
cut_facts_tac (Simplifier.prems_of_ss ss) i THEN 
760 
simpset_lin_arith_tac ss false i; 

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

761 

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

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

763 

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

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

765 
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

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

767 

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

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

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

770 

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

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

772 

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

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

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

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

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

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

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

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

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

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

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

783 

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

784 
fun splitasms (sg : theory) (asms : thm list) : splittree = 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

785 
let val {neqE, ...} = Data.get sg 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

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

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

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

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

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

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

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

793 
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

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

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

796 
in elim_neq ([], asms) end; 
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 
fun fwdproof (ctxt : theory * simpset) (Tip asms : splittree) (j::js : injust list) = 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

799 
(mkthm ctxt asms j, js) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

800 
 fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js = 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

801 
let val (thm1, js1) = fwdproof ctxt tree1 js 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

802 
val (thm2, js2) = fwdproof ctxt tree2 js1 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

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

804 
val thm2' = implies_intr ct2 thm2 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

805 
in (thm2' COMP (thm1' COMP thm), js2) end; 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

806 
(* needs handle THM _ => NONE ? *) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

807 

20268  808 
fun prover (ctxt as (sg, ss)) thms (Tconcl : term) (js : injust list) (pos : bool) : thm option = 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

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

810 
(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

811 
(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

812 
(* but beware: this can be a significant performance issue. *) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

813 
(* There is no "forward version" of 'pre_tac'. Therefore we combine the *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

814 
(* available theorems into a single proof state and perform "backward proof" *) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

815 
(* using 'refute_tac'. *) 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

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

817 
val Hs = map prop_of thms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

818 
val Prop = fold (curry Logic.mk_implies) (rev Hs) Tconcl 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

819 
val cProp = cterm_of sg Prop 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

820 
val concl = Goal.init cProp 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

821 
> refute_tac ss (1, js) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

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

824 
> fold (fn thA => fn thAB => implies_elim thAB thA) thms 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

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

826 
(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

827 
val nTconcl = LA_Logic.neg_prop Tconcl 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

828 
val cnTconcl = cterm_of sg nTconcl 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

829 
val nTconclthm = assume cnTconcl 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

830 
val tree = splitasms sg (thms @ [nTconclthm]) 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

831 
val (Falsethm, _) = fwdproof ctxt tree js 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

832 
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI 
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

833 
val concl = implies_intr cnTconcl Falsethm COMP contr 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

834 
in SOME (trace_thm "Proved by lin. arith. prover:" 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

836 
(* in case concl contains ?var, which makes assume fail: *) 
15531  837 
handle THM _ => NONE; 
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

838 

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

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

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

841 
1. lin_arith_prover tries both to prove and disprove concl and 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

842 
2. lin_arith_prover is applied by the simplifier which 
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset

843 
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

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

845 

20268  846 
fun lin_arith_prover sg ss (concl : term) : thm option = 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

847 
let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss)); 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

848 
val Hs = map prop_of thms 
6102  849 
val Tconcl = LA_Logic.mk_Trueprop concl 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

851 
val _ = trace_msg "lin_arith_prover" 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

852 
val _ = map (trace_thm "thms:") thms 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

853 
val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl) 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

855 
in case prove sg [] false false Hs Tconcl of (* concl provable? *) 
17515  856 
SOME js => prover (sg, ss) thms Tconcl js true 
15531  857 
 NONE => let val nTconcl = LA_Logic.neg_prop Tconcl 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

858 
in case prove sg [] false false Hs nTconcl of (* ~concl provable? *) 
17515  859 
SOME js => prover (sg, ss) thms nTconcl js false 
15531  860 
 NONE => NONE 
6079  861 
end 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

862 
end; 
6074  863 

864 
end; 