author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 40316  665862241968 
child 41493  f05976d69141 
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 

38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

91 
val map_data: 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

92 
({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

93 
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

94 
number_of: (theory > typ > int > cterm) option} > 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

95 
{add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

96 
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

97 
number_of: (theory > typ > int > cterm) option}) > 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

98 
Context.generic > Context.generic 
38762
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

99 
val add_inj_thms: thm list > Context.generic > Context.generic 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

100 
val add_lessD: thm > Context.generic > Context.generic 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

101 
val add_simps: thm list > Context.generic > Context.generic 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

102 
val add_simprocs: simproc list > Context.generic > Context.generic 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

103 
val set_number_of: (theory > typ > int > cterm) > Context.generic > Context.generic 
32740  104 
val trace: bool Unsynchronized.ref 
6062  105 
end; 
106 

24076  107 
functor Fast_Lin_Arith 
108 
(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

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

110 

9420  111 

112 
(** theory data **) 

113 

33519  114 
structure Data = Generic_Data 
22846  115 
( 
24076  116 
type T = 
117 
{add_mono_thms: thm list, 

118 
mult_mono_thms: thm list, 

119 
inj_thms: thm list, 

120 
lessD: thm list, 

121 
neqE: thm list, 

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

122 
simpset: Simplifier.simpset, 
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

123 
number_of: (theory > typ > int > cterm) option}; 
9420  124 

38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

125 
val empty : T = 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

126 
{add_mono_thms = [], mult_mono_thms = [], inj_thms = [], 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

127 
lessD = [], neqE = [], simpset = Simplifier.empty_ss, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

128 
number_of = NONE}; 
16458  129 
val extend = I; 
33519  130 
fun merge 
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

131 
({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

132 
lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1}, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

133 
{add_mono_thms = add_mono_thms2, mult_mono_thms = mult_mono_thms2, inj_thms = inj_thms2, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

134 
lessD = lessD2, neqE = neqE2, simpset = simpset2, number_of = number_of2}) : T = 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset

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

136 
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

137 
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

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

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

140 
simpset = Simplifier.merge_ss (simpset1, simpset2), 
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

141 
number_of = if is_some number_of1 then number_of1 else number_of2}; 
22846  142 
); 
9420  143 

144 
val map_data = Data.map; 

24076  145 
val get_data = Data.get o Context.Proof; 
9420  146 

38762
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

147 
fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

148 
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms, 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

149 
lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of}; 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

150 

996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

151 
fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

152 
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

153 
lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of}; 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

154 

996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

155 
fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

156 
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

157 
lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of}; 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

158 

996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

159 
fun add_inj_thms thms = map_data (map_inj_thms (append thms)); 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

160 
fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm])); 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

161 
fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms)); 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

162 
fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs)); 
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset

163 

38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

164 
fun set_number_of f = 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

165 
map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} => 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

166 
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

167 
lessD = lessD, neqE = neqE, simpset = simpset, number_of = SOME f}); 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

168 

283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

169 
fun number_of ctxt = 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

170 
(case Data.get (Context.Proof ctxt) of 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

171 
{number_of = SOME f, ...} => f (ProofContext.theory_of ctxt) 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

172 
 _ => fn _ => fn _ => raise CTERM ("number_of", [])); 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

173 

9420  174 

175 

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

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

177 
(*** Code ported from HOL Light ***) 
6056  178 
(* possible optimizations: 
179 
use (var,coeff) rep or vector rep tp save space; 

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

181 
*) 

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

182 

32740  183 
val trace = Unsynchronized.ref false; 
9073  184 

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

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

186 

6056  187 
datatype injust = Asm of int 
188 
 Nat of int (* index of atom *) 

6128  189 
 LessD of injust 
190 
 NotLessD of injust 

191 
 NotLeD of injust 

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

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

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

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

195 

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

196 
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

197 

13498  198 
(*  *) 
199 
(* Finding a (counter) example from the trace of a failed elimination *) 

200 
(*  *) 

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

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

203 

204 
exception NoEx; 

205 

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

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

207 
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

208 
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

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

210 

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

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

13498  214 

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

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

216 
fun eval ex v (a, le, cs) = 
22950  217 
let 
218 
val rs = map Rat.rat_of_int cs; 

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

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

222 
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

223 
*) 
13498  224 

22950  225 
fun ratrelmin2 (x as (r, ler), y as (s, les)) = 
23520  226 
case Rat.ord (r, s) 
22950  227 
of EQUAL => (r, (not ler) andalso (not les)) 
228 
 LESS => x 

229 
 GREATER => y; 

230 

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

23520  232 
case Rat.ord (r, s) 
22950  233 
of EQUAL => (r, ler andalso les) 
234 
 LESS => y 

235 
 GREATER => x; 

13498  236 

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

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

238 
val ratrelmax = foldr1 ratrelmax2; 
13498  239 

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

241 
if exact then r else 
22950  242 
let 
38052  243 
val (_, q) = Rat.quotient_of_rat r; 
22950  244 
val nth = Rat.inv (Rat.rat_of_int q); 
245 
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

246 

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

248 

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

249 
fun choose2 d ((lb, exactl), (ub, exactu)) = 
23520  250 
let val ord = Rat.sign lb in 
22950  251 
if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu) 
252 
then Rat.zero 

253 
else if not d then 

254 
if ord = GREATER 

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

255 
then if exactl then lb else ratmiddle (lb, ub) 
22950  256 
else if exactu then ub else ratmiddle (lb, ub) 
257 
else (*discrete domain, both bounds must be exact*) 

23025  258 
if ord = GREATER 
22950  259 
then let val lb' = Rat.roundup lb in 
260 
if Rat.le lb' ub then lb' else raise NoEx end 

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

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

263 
end; 

13498  264 

22950  265 
fun findex1 discr (v, lineqs) ex = 
266 
let 

23063  267 
val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs; 
22950  268 
val ineqs = maps elim_eqns nz; 
23063  269 
val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs 
22950  270 
val lb = ratrelmax (map (eval ex v) ge) 
271 
val ub = ratrelmin (map (eval ex v) le) 

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

274 
fun elim1 v x = 

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

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

13498  281 

282 
(* The base case: 

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

284 
fun pick_vars discr (ineqs,ex) = 

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

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

287 
 (_,_,cs) :: _ => 
23520  288 
let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs 
22950  289 
val d = nth discr v; 
23520  290 
val pos = not (Rat.sign (nth cs v) = LESS); 
22950  291 
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

292 
val minmax = 
17951  293 
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

294 
else ratexact true o ratrelmax 
17951  295 
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

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

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

301 
in pick_vars discr (ineqs',ex') end 
13498  302 
end; 
303 

304 
fun findex0 discr n lineqs = 

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

307 
ineqs 
17951  308 
in pick_vars discr (rineqs,replicate n Rat.zero) end; 
13498  309 

310 
(*  *) 

23197  311 
(* End of counterexample finder. The actual decision procedure starts here. *) 
13498  312 
(*  *) 
313 

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

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

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

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 find_add_type(Eq,x) = x 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

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

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

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

323 

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

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

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

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

327 

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

328 
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

329 
if n = 1 then i 
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset

330 
else if n = 0 andalso ty = Lt then raise Fail "multiply_ineq" 
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset

331 
else if n < 0 andalso (ty=Le orelse ty=Lt) then raise Fail "multiply_ineq" 
33002  332 
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

333 

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

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

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

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

337 

38052  338 
fun add_ineq (Lineq (k1,ty1,l1,just1)) (Lineq (k2,ty2,l2,just2)) = 
33002  339 
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

340 
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

341 

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

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

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

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

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

346 

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

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

350 
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

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

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

353 
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

354 
else if ty2 = Eq then (m1,~m2) 
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset

355 
else raise Fail "elim_var" 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

357 
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

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

359 
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

360 

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

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

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

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

364 

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

365 
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

366 

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

368 
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

369 

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

370 
fun calc_blowup l = 
33317  371 
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

372 
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

373 

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

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

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

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

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

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

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

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

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

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

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

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

385 

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

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

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

388 
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

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

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

391 

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

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

397 
commas(map string_of_int l)) ineqs)) 
9073  398 
else (); 
6056  399 

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

402 

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

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

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

405 
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

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

407 
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

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

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

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

413 
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

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

415 
let val c = 
33042  416 
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

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

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

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

420 
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

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

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

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

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

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

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

432 
val iblows = blows ~~ numlist 
23063  433 
val nziblows = filter_out (fn (i, _) => i = 0) iblows 
13498  434 
in if null nziblows then Failure((~1,nontriv)::hist) 
435 
else 

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

436 
let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) 
23063  437 
val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs 
438 
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

439 
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

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

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

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

443 

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

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

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

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

447 

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

448 
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

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

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

454 
fun trace_msg msg = 

455 
if !trace then tracing msg else (); 

9073  456 

33042  457 
val union_term = union Pattern.aeconv; 
458 
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

459 

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

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

461 
union_term (map fst lhs) o union_term (map fst rhs); 
6056  462 

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

463 
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

464 

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

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

468 
with 0 <= n. 

469 
*) 

470 
local 

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

473 

24076  474 
fun mkthm ss asms (just: injust) = 
475 
let 

476 
val ctxt = Simplifier.the_context ss; 

477 
val thy = ProofContext.theory_of ctxt; 

38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

478 
val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; 
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

479 
val number_of = number_of ctxt; 
24076  480 
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

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

482 
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

483 
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

484 

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

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

486 
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

487 

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

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

489 
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

490 
fun try_add thms thm = get_first (fn th => add2 th thm) thms; 
6056  491 

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

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

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

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

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

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

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

498 
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

499 
(trace_thm ctxt "" thm1; trace_thm ctxt "" thm2; 
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset

500 
raise Fail "Linear arithmetic: failed to add thms")) 
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset

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

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

503 

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

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

505 
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

506 
in mul n thm end; 
10575  507 

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

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

509 
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

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

511 
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

512 
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

513 
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

514 

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

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

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

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

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

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

520 
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

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

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

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

524 
mth 
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side  note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset

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

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

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

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

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

530 
end); 
10691  531 

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

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

533 
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

534 
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

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

536 

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

537 
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

538 
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

539 
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end; 
6056  540 

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

541 
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

542 
 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

543 
 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

544 
 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

545 
 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

546 
 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

547 
 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

548 
 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

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

550 

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

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

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

553 
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

554 
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

555 
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

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

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

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

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

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

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

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

563 
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

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

565 
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

566 
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

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

568 

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

570 

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

572 
AList.lookup Pattern.aeconv poly atom > the_default 0; 
10691  573 

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

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

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

579 
in (t,i * (m div j)) end 
12932  580 
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end 
10691  581 

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

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

584 
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item 
13498  585 
val lhsa = map (coeff lhs) atoms 
586 
and rhsa = map (coeff rhs) atoms 

18330  587 
val diff = map2 (curry (op )) rhsa lhsa 
13498  588 
val c = ij 
589 
val just = Asm k 

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

593 
 "~<=" => if discrete 

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

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

596 
 "<" => if discrete 

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

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

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

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

40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset

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

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

603 

13498  604 
(*  *) 
605 
(* Print (counter) example *) 

606 
(*  *) 

607 

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

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

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

612 
else string_of_int p ^ "/" ^ string_of_int q 
13498  613 
in a ^ " = " ^ s end; 
614 

19049  615 
fun produce_ex sds = 
17496  616 
curry (op ~~) sds 
617 
#> map print_atom 

618 
#> commas 

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

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

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

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

624 
 (v, lineqs) :: hist' => 
24076  625 
let 
626 
val frees = map Free params 

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

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

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

633 
handle NoEx => NONE 
24076  634 
in 
635 
case ex of 

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

24076  638 
end; 
13498  639 

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

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

641 

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

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

645 
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

646 
else NONE; 
6056  647 

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

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

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

653 
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

654 
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

655 
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

656 
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

657 

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

658 
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

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

660 

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

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

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

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

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

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

666 

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

667 
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

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

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

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

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

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

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

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

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

676 
(* can be applied, and split the premise accordingly. *) 
26945  677 
fun elim_neq (ineqs : (LA_Data.decomp option * bool) list) : 
678 
(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

679 
let 
26945  680 
fun elim_neq' nat_only ([] : (LA_Data.decomp option * bool) list) : 
681 
(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

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

683 
 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

684 
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

685 
 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

686 
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

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

688 
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

689 
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

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

691 
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

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

693 
ineqs > elim_neq' true 
26945  694 
> 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

695 
end 
13464  696 

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

697 
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

698 
 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

699 
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

700 

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

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

702 
 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

703 
 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

704 

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

705 
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

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

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

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

713 
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

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

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

717 
map (apsnd (number_hyps 0)) 
23195  718 
in 
719 
trace_msg ("Splitting of inequalities yields " ^ 

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

721 
result 

722 
end; 

13464  723 

33245  724 
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

725 
union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); 
13498  726 

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

729 

24076  730 
fun refutes ctxt params show_ex : 
26945  731 
(typ list * (LA_Data.decomp * int) list) list > injust list > injust list option = 
732 
let 

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

734 
let 

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

735 
val atoms = atoms_of (map fst initems) 
26945  736 
val n = length atoms 
38052  737 
val mkleq = mklineq atoms 
26945  738 
val ixs = 0 upto (n  1) 
739 
val iatoms = atoms ~~ ixs 

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

743 
Success j => 

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

745 
refute initemss (js @ [j])) 

746 
 Failure hist => 

747 
(if not show_ex then () 

748 
else 

749 
let 

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

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

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

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

754 
in 

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

756 
end; NONE) 

757 
end 

758 
 refute [] js = SOME js 

759 
in refute end; 

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

760 

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

761 
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

762 
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

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

764 

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

766 

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

767 
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

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

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

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

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

773 
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

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

775 
 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

776 
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

777 
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

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

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

781 
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

782 
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

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

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

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

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

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

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

791 

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

792 
fun refute_tac ss (i, split_neq, justs) = 
6074  793 
fn state => 
24076  794 
let 
795 
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

796 
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

797 
("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

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

801 
(* eliminate inequalities *) 

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

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

803 
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

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

805 
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

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

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

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

813 
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

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

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

817 
end state; 
6074  818 

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

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

820 
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

821 
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

822 
*) 
24076  823 
fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => 
824 
let 

825 
val ctxt = Simplifier.the_context ss 

826 
val params = rev (Logic.strip_params A) 

827 
val Hs = Logic.strip_assums_hyp A 

828 
val concl = Logic.strip_assums_concl A 

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

830 
in 

831 
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

832 
(_, 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

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

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

836 

24076  837 
fun cut_lin_arith_tac ss = 
838 
cut_facts_tac (Simplifier.prems_of_ss ss) THEN' 

839 
simpset_lin_arith_tac ss false; 

17613  840 

24076  841 
fun lin_arith_tac ctxt = 
842 
simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); 

843 

844 

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

845 

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

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

847 

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

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

849 
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

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

851 

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

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

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

854 

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

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

856 

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

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

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

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

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

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

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

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

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

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

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

867 

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

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

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

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

872 
 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

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

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

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

876 
let val (ct1, ct2) = extract (cprop_of spl) 
36945  877 
val thm1 = Thm.assume ct1 
878 
val thm2 = Thm.assume ct2 

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

879 
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

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

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

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

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

884 

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

887 
let 

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

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

36945  890 
val thm1' = Thm.implies_intr ct1 thm1 
891 
val thm2' = Thm.implies_intr ct2 thm2 

24076  892 
in (thm2' COMP (thm1' COMP thm), js2) end; 
893 
(* FIXME needs handle THM _ => NONE ? *) 

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

894 

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

895 
fun prover ss thms Tconcl (js : injust list) split_neq pos : thm option = 
24076  896 
let 
897 
val ctxt = Simplifier.the_context ss 

898 
val thy = ProofContext.theory_of ctxt 

899 
val nTconcl = LA_Logic.neg_prop Tconcl 

900 
val cnTconcl = cterm_of thy nTconcl 

36945  901 
val nTconclthm = Thm.assume cnTconcl 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

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

36945  905 
val concl = Thm.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

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

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

909 

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

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

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

914 
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

915 
*) 
24076  916 
fun lin_arith_simproc ss concl = 
917 
let 

918 
val ctxt = Simplifier.the_context ss 

26945  919 
val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss) 
24076  920 
val Hs = map Thm.prop_of thms 
6102  921 
val Tconcl = LA_Logic.mk_Trueprop concl 
24076  922 
in 
923 
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

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

925 
 (_, NONE) => 
24076  926 
let val nTconcl = LA_Logic.neg_prop Tconcl in 
927 
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

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

929 
 (_, NONE) => NONE 
24076  930 
end 
931 
end; 

6074  932 

933 
end; 