author  haftmann 
Wed, 05 May 2010 18:25:34 +0200  
changeset 36692  54b64d4ad524 
parent 35872  9b579860d59b 
child 36945  9bec62c10714 
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 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

2 
Author: Tobias Nipkow and Tjark Weber and Sascha Boehme 
6102  3 

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

6 
(lin_arith_simproc). 

6102  7 

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

10 
the term. 

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

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

12 

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

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

14 

6102  15 
signature LIN_ARITH_LOGIC = 
16 
sig 

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

17 
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

18 
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

19 
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

20 
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

21 
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

22 
val sym : thm (* x = y ==> y = x *) 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

23 
val trueI : thm (* True *) 
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

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

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

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

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

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

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

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

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

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

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

36 

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

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

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

41 
the form 'Trueprop $ _' 

6128  42 

43 
is_nat(parametertypes,t) = t:nat 

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

6102  45 
*) 
46 

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

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

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

24076  52 
val domain_is_nat: term > bool 
53 

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

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

56 

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

35230
be006fbcfb96
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
wenzelm
parents:
33519
diff
changeset

58 
val pre_tac: simpset > int > tactic 
24076  59 

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

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

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

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

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

65 
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

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

67 
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

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

69 
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

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

71 

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

72 
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

73 

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

74 
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

75 
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

76 
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

77 
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

78 
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

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

80 

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

82 
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

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

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

85 

6062  86 
signature FAST_LIN_ARITH = 
87 
sig 

31102  88 
val cut_lin_arith_tac: simpset > int > tactic 
89 
val lin_arith_tac: Proof.context > bool > int > tactic 

90 
val lin_arith_simproc: simpset > term > thm option 

15184  91 
val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

92 
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

93 
number_of : serial * (theory > typ > int > cterm)} 
15184  94 
> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

95 
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

96 
number_of : serial * (theory > typ > int > cterm)}) 
24076  97 
> Context.generic > Context.generic 
32740  98 
val trace: bool Unsynchronized.ref 
6062  99 
end; 
100 

24076  101 
functor Fast_Lin_Arith 
102 
(structure LA_Logic: LIN_ARITH_LOGIC and LA_Data: LIN_ARITH_DATA): FAST_LIN_ARITH = 

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

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

104 

9420  105 

106 
(** theory data **) 

107 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

108 
fun no_number_of _ _ _ = raise CTERM ("number_of", []) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

109 

33519  110 
structure Data = Generic_Data 
22846  111 
( 
24076  112 
type T = 
113 
{add_mono_thms: thm list, 

114 
mult_mono_thms: thm list, 

115 
inj_thms: thm list, 

116 
lessD: thm list, 

117 
neqE: thm list, 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

118 
simpset: Simplifier.simpset, 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

119 
number_of : serial * (theory > typ > int > cterm)}; 
9420  120 

10691  121 
val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

122 
lessD = [], neqE = [], simpset = Simplifier.empty_ss, 
31638  123 
number_of = (serial (), no_number_of) } : T; 
16458  124 
val extend = I; 
33519  125 
fun merge 
16458  126 
({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

127 
lessD = lessD1, neqE=neqE1, simpset = simpset1, 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

128 
number_of = (number_of1 as (s1, _))}, 
16458  129 
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

130 
lessD = lessD2, neqE=neqE2, simpset = simpset2, 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

131 
number_of = (number_of2 as (s2, _))}) = 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

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

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

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

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

136 
neqE = Thm.merge_thms (neqE1, neqE2), 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

137 
simpset = Simplifier.merge_ss (simpset1, simpset2), 
33519  138 
(* FIXME depends on accidental load order !?! *) 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

139 
number_of = if s1 > s2 then number_of1 else number_of2}; 
22846  140 
); 
9420  141 

142 
val map_data = Data.map; 

24076  143 
val get_data = Data.get o Context.Proof; 
9420  144 

145 

146 

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

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

148 
(*** Code ported from HOL Light ***) 
6056  149 
(* possible optimizations: 
150 
use (var,coeff) rep or vector rep tp save space; 

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

152 
*) 

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

153 

32740  154 
val trace = Unsynchronized.ref false; 
9073  155 

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

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

157 

6056  158 
datatype injust = Asm of int 
159 
 Nat of int (* index of atom *) 

6128  160 
 LessD of injust 
161 
 NotLessD of injust 

162 
 NotLeD of injust 

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

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

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

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

166 

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

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

168 

13498  169 
(*  *) 
170 
(* Finding a (counter) example from the trace of a failed elimination *) 

171 
(*  *) 

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

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

174 

175 
exception NoEx; 

176 

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

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

178 
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

179 
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

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

181 

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

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

13498  185 

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

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

187 
fun eval ex v (a, le, cs) = 
22950  188 
let 
189 
val rs = map Rat.rat_of_int cs; 

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

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

193 
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

194 
*) 
13498  195 

22950  196 
fun ratrelmin2 (x as (r, ler), y as (s, les)) = 
23520  197 
case Rat.ord (r, s) 
22950  198 
of EQUAL => (r, (not ler) andalso (not les)) 
199 
 LESS => x 

200 
 GREATER => y; 

201 

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

23520  203 
case Rat.ord (r, s) 
22950  204 
of EQUAL => (r, ler andalso les) 
205 
 LESS => y 

206 
 GREATER => x; 

13498  207 

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

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

209 
val ratrelmax = foldr1 ratrelmax2; 
13498  210 

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

212 
if exact then r else 
22950  213 
let 
214 
val (p, q) = Rat.quotient_of_rat r; 

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

216 
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

217 

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

219 

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

220 
fun choose2 d ((lb, exactl), (ub, exactu)) = 
23520  221 
let val ord = Rat.sign lb in 
22950  222 
if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu) 
223 
then Rat.zero 

224 
else if not d then 

225 
if ord = GREATER 

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

226 
then if exactl then lb else ratmiddle (lb, ub) 
22950  227 
else if exactu then ub else ratmiddle (lb, ub) 
228 
else (*discrete domain, both bounds must be exact*) 

23025  229 
if ord = GREATER 
22950  230 
then let val lb' = Rat.roundup lb in 
231 
if Rat.le lb' ub then lb' else raise NoEx end 

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

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

234 
end; 

13498  235 

22950  236 
fun findex1 discr (v, lineqs) ex = 
237 
let 

23063  238 
val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs; 
22950  239 
val ineqs = maps elim_eqns nz; 
23063  240 
val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs 
22950  241 
val lb = ratrelmax (map (eval ex v) ge) 
242 
val ub = ratrelmin (map (eval ex v) le) 

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

245 
fun elim1 v x = 

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

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

13498  252 

253 
(* The base case: 

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

255 
fun pick_vars discr (ineqs,ex) = 

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

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

258 
 (_,_,cs) :: _ => 
23520  259 
let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs 
22950  260 
val d = nth discr v; 
23520  261 
val pos = not (Rat.sign (nth cs v) = LESS); 
22950  262 
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

263 
val minmax = 
17951  264 
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

265 
else ratexact true o ratrelmax 
17951  266 
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

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

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

272 
in pick_vars discr (ineqs',ex') end 
13498  273 
end; 
274 

275 
fun findex0 discr n lineqs = 

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

278 
ineqs 
17951  279 
in pick_vars discr (rineqs,replicate n Rat.zero) end; 
13498  280 

281 
(*  *) 

23197  282 
(* End of counterexample finder. The actual decision procedure starts here. *) 
13498  283 
(*  *) 
284 

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

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

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

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

288 

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

289 
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

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

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

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

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

294 

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

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

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

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

298 

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

299 
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

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

301 
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

302 
else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq" 
33002  303 
else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just)); 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

304 

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

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

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

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

308 

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

309 
fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 
33002  310 
let val l = map2 Integer.add l1 l2 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

311 
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

312 

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

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

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

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

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

317 

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

318 
fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 
23063  319 
let val c1 = nth l1 v and c2 = nth l2 v 
23261  320 
val m = Integer.lcm (abs c1) (abs c2) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

321 
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

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

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

324 
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

325 
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

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

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

328 
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

329 
then (~n1,~n2) else (n1,n2) 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

330 
in add_ineq (multiply_ineq p1 i1) (multiply_ineq p2 i2) end; 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

331 

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

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

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

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

336 
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

337 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

338 
fun is_contradictory (ans as Lineq(k,ty,l,_)) = 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

339 
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

340 

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

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

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

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

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

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

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

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

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

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

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

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

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

356 

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

357 
fun extract_first p = 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

358 
let 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

359 
fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

360 
 extract xs [] = raise Empty 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

362 

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

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

368 
commas(map string_of_int l)) ineqs)) 
9073  369 
else (); 
6056  370 

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

373 

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

374 
fun elim (ineqs, hist) = 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

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

376 
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

377 
if not (null triv) 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

378 
then case Library.find_first is_contradictory triv of 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

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

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

384 
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

385 
if not (null eqs) then 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

386 
let val c = 
33042  387 
fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

388 
> filter (fn i => i <> 0) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

389 
> sort (int_ord o pairself abs) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

390 
> hd 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

391 
val (eq as Lineq(_,_,ceq,_),othereqs) = 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35872
diff
changeset

392 
extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs 
31986  393 
val v = find_index (fn v => v = c) ceq 
23063  394 
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

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

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

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

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

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

403 
val iblows = blows ~~ numlist 
23063  404 
val nziblows = filter_out (fn (i, _) => i = 0) iblows 
13498  405 
in if null nziblows then Failure((~1,nontriv)::hist) 
406 
else 

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

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

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

410 
in elim(no @ map_product (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

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

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

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

414 

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

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

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

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

418 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

419 
fun trace_thm ctxt msg th = 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

420 
(if !trace then (tracing msg; tracing (Display.string_of_thm ctxt th)) else (); th); 
9073  421 

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

425 
fun trace_msg msg = 

426 
if !trace then tracing msg else (); 

9073  427 

33042  428 
val union_term = union Pattern.aeconv; 
429 
val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')); 

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

430 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

431 
fun add_atoms (lhs, _, _, rhs, _, _) = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

432 
union_term (map fst lhs) o union_term (map fst rhs); 
6056  433 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

434 
fun atoms_of ds = fold add_atoms ds []; 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

435 

e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

436 
(* 
6056  437 
Simplification may detect a contradiction 'prematurely' due to type 
438 
information: n+1 <= 0 is simplified to False and does not need to be crossed 

439 
with 0 <= n. 

440 
*) 

441 
local 

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

444 

24076  445 
fun mkthm ss asms (just: injust) = 
446 
let 

447 
val ctxt = Simplifier.the_context ss; 

448 
val thy = ProofContext.theory_of ctxt; 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

449 
val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

450 
number_of = (_, num_of), ...} = get_data ctxt; 
24076  451 
val simpset' = Simplifier.inherit_context ss simpset; 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

452 
fun only_concl f thm = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

453 
if Thm.no_prems thm then f (Thm.concl_of thm) else NONE; 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

454 
val atoms = atoms_of (map_filter (only_concl (LA_Data.decomp ctxt)) asms); 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

455 

e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

456 
fun use_first rules thm = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

457 
get_first (fn th => SOME (thm RS th) handle THM _ => NONE) rules 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

458 

e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

459 
fun add2 thm1 thm2 = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

460 
use_first add_mono_thms (thm1 RS (thm2 RS LA_Logic.conjI)); 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

461 
fun try_add thms thm = get_first (fn th => add2 th thm) thms; 
6056  462 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

463 
fun add_thms thm1 thm2 = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

464 
(case add2 thm1 thm2 of 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

465 
NONE => 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

466 
(case try_add ([thm1] RL inj_thms) thm2 of 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

467 
NONE => 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

468 
(the (try_add ([thm2] RL inj_thms) thm1) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

469 
handle Option => 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

470 
(trace_thm ctxt "" thm1; trace_thm ctxt "" thm2; 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

471 
sys_error "Linear arithmetic: failed to add thms")) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

472 
 SOME thm => thm) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

473 
 SOME thm => thm); 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

474 

e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

475 
fun mult_by_add n thm = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

476 
let fun mul i th = if i = 1 then th else mul (i  1) (add_thms thm th) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

477 
in mul n thm end; 
10575  478 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

479 
val rewr = Simplifier.rewrite simpset'; 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

480 
val rewrite_concl = Conv.fconv_rule (Conv.concl_conv ~1 (Conv.arg_conv 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

481 
(Conv.binop_conv rewr))); 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

482 
fun discharge_prem thm = if Thm.nprems_of thm = 0 then thm else 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

483 
let val cv = Conv.arg1_conv (Conv.arg_conv rewr) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

484 
in Thm.implies_elim (Conv.fconv_rule cv thm) LA_Logic.trueI end 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

485 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

486 
fun mult n thm = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

487 
(case use_first mult_mono_thms thm of 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

488 
NONE => mult_by_add n thm 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

489 
 SOME mth => 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

490 
let 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

491 
val cv = mth > Thm.cprop_of > Drule.strip_imp_concl 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

492 
> Thm.dest_arg > Thm.dest_arg1 > Thm.dest_arg1 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

493 
val T = #T (Thm.rep_cterm cv) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

494 
in 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

495 
mth 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

496 
> Thm.instantiate ([], [(cv, num_of thy T n)]) 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

497 
> rewrite_concl 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

498 
> discharge_prem 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

499 
handle CTERM _ => mult_by_add n thm 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

500 
 THM _ => mult_by_add n thm 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

501 
end); 
10691  502 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

503 
fun mult_thm (n, thm) = 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

504 
if n = ~1 then thm RS LA_Logic.sym 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

505 
else if n < 0 then mult (~n) thm RS LA_Logic.sym 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

506 
else mult n thm; 
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

507 

e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

508 
fun simp thm = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

509 
let val thm' = trace_thm ctxt "Simplified:" (full_simplify simpset' thm) 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

510 
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end; 
6056  511 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

512 
fun mk (Asm i) = trace_thm ctxt ("Asm " ^ string_of_int i) (nth asms i) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

513 
 mk (Nat i) = trace_thm ctxt ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i)) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

514 
 mk (LessD j) = trace_thm ctxt "L" (hd ([mk j] RL lessD)) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

515 
 mk (NotLeD j) = trace_thm ctxt "NLe" (mk j RS LA_Logic.not_leD) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

516 
 mk (NotLeDD j) = trace_thm ctxt "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

517 
 mk (NotLessD j) = trace_thm ctxt "NL" (mk j RS LA_Logic.not_lessD) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

518 
 mk (Added (j1, j2)) = simp (trace_thm ctxt "+" (add_thms (mk j1) (mk j2))) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

519 
 mk (Multiplied (n, j)) = 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

520 
(trace_msg ("*" ^ string_of_int n); trace_thm ctxt "*" (mult_thm (n, mk j))) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

521 

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

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

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

524 
val _ = trace_msg "mkthm"; 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

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

526 
val fls = simplify simpset' thm; 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

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

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

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

530 
else 
35872
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset

531 
(tracing (cat_lines 
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset

532 
(["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @ 
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset

533 
["Proved:", Display.string_of_thm ctxt fls, ""])); 
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset

534 
warning "Linear arithmetic should have refuted the assumptions.\n\ 
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset

535 
\Please inform Tobias Nipkow.") 
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

536 
in fls end 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

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

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

539 

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

541 

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

543 
AList.lookup Pattern.aeconv poly atom > the_default 0; 
10691  544 

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

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

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

550 
in (t,i * (m div j)) end 
12932  551 
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end 
10691  552 

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

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

555 
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item 
13498  556 
val lhsa = map (coeff lhs) atoms 
557 
and rhsa = map (coeff rhs) atoms 

18330  558 
val diff = map2 (curry (op )) rhsa lhsa 
13498  559 
val c = ij 
560 
val just = Asm k 

31511  561 
fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied(m,j)) 
13498  562 
in case rel of 
563 
"<=" => lineq(c,Le,diff,just) 

564 
 "~<=" => if discrete 

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

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

567 
 "<" => if discrete 

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

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

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

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

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

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

574 

13498  575 
(*  *) 
576 
(* Print (counter) example *) 

577 
(*  *) 

578 

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

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

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

583 
else string_of_int p ^ "/" ^ string_of_int q 
13498  584 
in a ^ " = " ^ s end; 
585 

19049  586 
fun produce_ex sds = 
17496  587 
curry (op ~~) sds 
588 
#> map print_atom 

589 
#> commas 

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

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

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

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

595 
 (v, lineqs) :: hist' => 
24076  596 
let 
597 
val frees = map Free params 

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

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

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

604 
handle NoEx => NONE 
24076  605 
in 
606 
case ex of 

30687  607 
SOME s => (warning "Linear arithmetic failed  see trace for a counterexample."; tracing s) 
608 
 NONE => warning "Linear arithmetic failed" 

24076  609 
end; 
13498  610 

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

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

612 

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

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

616 
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

617 
else NONE; 
6056  618 

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

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

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

624 
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

625 
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

626 
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

627 
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

628 

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

629 
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

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

631 

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

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

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

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

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

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

637 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

650 
let 
26945  651 
fun elim_neq' nat_only ([] : (LA_Data.decomp option * bool) list) : 
652 
(LA_Data.decomp option * bool) list list = 

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

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

654 
 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

655 
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

656 
 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

657 
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

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

659 
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

660 
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

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

662 
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

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

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

666 
end 
13464  667 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

668 
fun ignore_neq (NONE, bool) = (NONE, bool) 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

669 
 ignore_neq (ineq as SOME (_, _, rel, _, _, _), bool) = 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

670 
if rel = "~=" then (NONE, bool) else (ineq, bool) 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

671 

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

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

673 
 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

674 
 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

675 

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

676 
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

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

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

683 
> (* splitting of inequalities *) 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

684 
map (apsnd (if split_neq then elim_neq else 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

685 
Library.single o map ignore_neq)) 
22846  686 
> 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

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

688 
map (apsnd (number_hyps 0)) 
23195  689 
in 
690 
trace_msg ("Splitting of inequalities yields " ^ 

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

692 
result 

693 
end; 

13464  694 

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

696 
union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); 
13498  697 

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

700 

24076  701 
fun refutes ctxt params show_ex : 
26945  702 
(typ list * (LA_Data.decomp * int) list) list > injust list > injust list option = 
703 
let 

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

705 
let 

31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

706 
val atoms = atoms_of (map fst initems) 
26945  707 
val n = length atoms 
708 
val mkleq = mklineq n atoms 

709 
val ixs = 0 upto (n  1) 

710 
val iatoms = atoms ~~ ixs 

32952  711 
val natlineqs = map_filter (mknat Ts ixs) iatoms 
26945  712 
val ineqs = map mkleq initems @ natlineqs 
713 
in case elim (ineqs, []) of 

714 
Success j => 

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

716 
refute initemss (js @ [j])) 

717 
 Failure hist => 

718 
(if not show_ex then () 

719 
else 

720 
let 

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

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

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

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

725 
in 

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

727 
end; NONE) 

728 
end 

729 
 refute [] js = SOME js 

730 
in refute end; 

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

731 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

732 
fun refute ctxt params show_ex do_pre split_neq terms : injust list option = 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

733 
refutes ctxt params show_ex (split_items ctxt do_pre split_neq 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

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

735 

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

737 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

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

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

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

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

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

744 
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

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

746 
 is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

747 
val neq_limit = Config.get ctxt LA_Data.fast_arith_neq_limit 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

748 
val split_neq = count is_neq (map (LA_Data.decomp ctxt) Hs') <= neq_limit 
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset

749 
in 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

750 
if split_neq then () 
24076  751 
else 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

752 
trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

753 
string_of_int neq_limit ^ "), ignoring all inequalities"); 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

754 
(split_neq, refute ctxt params show_ex do_pre split_neq Hs') 
23190  755 
end handle TERM ("neg_prop", _) => 
756 
(* since no metalogic negation is available, we can only fail if *) 

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

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

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

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

760 
(trace_msg "prove failed (cannot negate conclusion)."; 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

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

762 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

763 
fun refute_tac ss (i, split_neq, justs) = 
6074  764 
fn state => 
24076  765 
let 
766 
val ctxt = Simplifier.the_context ss; 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

767 
val _ = trace_thm ctxt 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

768 
("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

769 
string_of_int (length justs) ^ " justification(s)):") state 
24076  770 
val {neqE, ...} = get_data ctxt; 
771 
fun just1 j = 

772 
(* eliminate inequalities *) 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

773 
(if split_neq then 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

774 
REPEAT_DETERM (eresolve_tac neqE i) 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

775 
else 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

776 
all_tac) THEN 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

777 
PRIMITIVE (trace_thm ctxt "State after neqE:") THEN 
24076  778 
(* use theorems generated from the actual justifications *) 
32283  779 
Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i 
24076  780 
in 
781 
(* rewrite "[ A1; ...; An ] ==> B" to "[ A1; ...; An; ~B ] ==> False" *) 

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

783 
(* userdefined preprocessing of the subgoal *) 

35230
be006fbcfb96
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
wenzelm
parents:
33519
diff
changeset

784 
DETERM (LA_Data.pre_tac ss i) THEN 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

785 
PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN 
24076  786 
(* prove every resulting subgoal, using its justification *) 
787 
EVERY (map just1 justs) 

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

788 
end state; 
6074  789 

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

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

791 
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

792 
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

793 
*) 
24076  794 
fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => 
795 
let 

796 
val ctxt = Simplifier.the_context ss 

797 
val params = rev (Logic.strip_params A) 

798 
val Hs = Logic.strip_assums_hyp A 

799 
val concl = Logic.strip_assums_concl A 

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

801 
in 

802 
case prove ctxt params show_ex true Hs concl of 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

803 
(_, NONE) => (trace_msg "Refutation failed."; no_tac) 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

804 
 (split_neq, SOME js) => (trace_msg "Refutation succeeded."; 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

805 
refute_tac ss (i, split_neq, js)) 
24076  806 
end); 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

807 

24076  808 
fun cut_lin_arith_tac ss = 
809 
cut_facts_tac (Simplifier.prems_of_ss ss) THEN' 

810 
simpset_lin_arith_tac ss false; 

17613  811 

24076  812 
fun lin_arith_tac ctxt = 
813 
simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); 

814 

815 

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

816 

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

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

818 

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

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

820 
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

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

822 

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

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

824 
 Spl of thm * cterm * splittree * cterm * splittree; 
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 
(* "(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

827 

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

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

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

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

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

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

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

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

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

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

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

838 

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

35693
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

841 
fun elim_neq [] (asms', []) = Tip (rev asms') 
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

842 
 elim_neq [] (asms', asms) = Tip (rev asms' @ asms) 
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

843 
 elim_neq (neq :: neqs) (asms', []) = elim_neq neqs ([],rev asms') 
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

844 
 elim_neq (neqs as (neq :: _)) (asms', asm::asms) = 
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

845 
(case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

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

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

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

849 
val thm2 = assume ct2 
35693
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

850 
in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]), 
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

851 
ct2, elim_neq neqs (asms', asms@[thm2])) 
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset

852 
end 
35693
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

853 
 NONE => elim_neq neqs (asm::asms', asms)) 
d58a4ac1ca1c
Use same order of neqelimination as in proof search.
hoelzl
parents:
35230
diff
changeset

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

855 

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

858 
let 

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

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

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

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

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

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

865 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

866 
fun prover ss thms Tconcl (js : injust list) split_neq pos : thm option = 
24076  867 
let 
868 
val ctxt = Simplifier.the_context ss 

869 
val thy = ProofContext.theory_of ctxt 

870 
val nTconcl = LA_Logic.neg_prop Tconcl 

871 
val cnTconcl = cterm_of thy nTconcl 

872 
val nTconclthm = assume cnTconcl 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

873 
val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm]) 
24076  874 
val (Falsethm, _) = fwdproof ss tree js 
875 
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI 

876 
val concl = implies_intr cnTconcl Falsethm COMP contr 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

877 
in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end 
24076  878 
(*in case concl contains ?var, which makes assume fail:*) (* FIXME Variable.import_terms *) 
879 
handle THM _ => NONE; 

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

880 

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

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

882 
This assumption is OK because 
24076  883 
1. lin_arith_simproc tries both to prove and disprove concl and 
884 
2. lin_arith_simproc is applied by the Simplifier which 

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

885 
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

886 
*) 
24076  887 
fun lin_arith_simproc ss concl = 
888 
let 

889 
val ctxt = Simplifier.the_context ss 

26945  890 
val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss) 
24076  891 
val Hs = map Thm.prop_of thms 
6102  892 
val Tconcl = LA_Logic.mk_Trueprop concl 
24076  893 
in 
894 
case prove ctxt [] false false Hs Tconcl of (* concl provable? *) 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

895 
(split_neq, SOME js) => prover ss thms Tconcl js split_neq true 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

896 
 (_, NONE) => 
24076  897 
let val nTconcl = LA_Logic.neg_prop Tconcl in 
898 
case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *) 

30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

899 
(split_neq, SOME js) => prover ss thms nTconcl js split_neq false 
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

900 
 (_, NONE) => NONE 
24076  901 
end 
902 
end; 

6074  903 

904 
end; 