author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 49387  167708456269 
child 51717  9e7d1c139569 
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 

46709
65a9b30bff00
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
wenzelm
parents:
44654
diff
changeset

4 
A generic linear arithmetic package. 
6102  5 

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

8 
the term. 

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

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

10 

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

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

12 

6102  13 
signature LIN_ARITH_LOGIC = 
14 
sig 

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

15 
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

16 
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

17 
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

18 
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

19 
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

20 
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

21 
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

22 
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

23 
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

24 
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

25 
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

26 
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

27 
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

28 
val mk_nat_thm : theory > term > thm 
6102  29 
end; 
30 
(* 

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

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

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

34 

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

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

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

39 
the form 'Trueprop $ _' 

6128  40 

41 
is_nat(parametertypes,t) = t:nat 

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

6102  43 
*) 
44 

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

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

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

24076  50 
val domain_is_nat: term > bool 
51 

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

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

54 

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

56 
val pre_tac: simpset > int > tactic 
24076  57 

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

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

44654  60 
val neq_limit: int Config.T 
43607
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

61 

44654  62 
val verbose: bool Config.T 
63 
val trace: bool Config.T 

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

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

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

66 
decomp(`x Rel y') should yield (p,i,Rel,q,j,d) 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

68 
p (q, respectively) is the decomposition of the sum term x 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

70 
pairs and a constant summand and d indicates if the domain 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

72 

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

73 
domain_is_nat(`x Rel y') t should yield true iff x is of type "nat". 
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset

74 

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

75 
The relationship between pre_decomp and pre_tac is somewhat tricky. The 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

76 
internal representation of a subgoal and the corresponding theorem must 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

77 
be modified by pre_decomp (pre_tac, resp.) in a corresponding way. See 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

78 
the comment for split_items below. (This is even necessary for eta and 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

79 
betaequivalent modifications, as some of the lin. arith. code is not 
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

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

81 

9420  82 
ss must reduce contradictory <= to False. 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

83 
It should also cancel common summands to keep <= reduced; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

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

86 

6062  87 
signature FAST_LIN_ARITH = 
88 
sig 

46709
65a9b30bff00
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
wenzelm
parents:
44654
diff
changeset

89 
val prems_lin_arith_tac: simpset > int > tactic 
31102  90 
val lin_arith_tac: Proof.context > bool > int > tactic 
91 
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

92 
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

93 
({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

94 
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

95 
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

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

97 
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

98 
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

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

100 
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

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

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

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

104 
val set_number_of: (theory > typ > int > cterm) > Context.generic > Context.generic 
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), 
41493  141 
number_of = merge_options (number_of1, 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 
42361  171 
{number_of = SOME f, ...} => f (Proof_Context.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

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 

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

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

184 

6056  185 
datatype injust = Asm of int 
186 
 Nat of int (* index of atom *) 

6128  187 
 LessD of injust 
188 
 NotLessD of injust 

189 
 NotLeD of injust 

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

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

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

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

193 

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

194 
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

195 

13498  196 
(*  *) 
197 
(* Finding a (counter) example from the trace of a failed elimination *) 

198 
(*  *) 

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

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

201 

202 
exception NoEx; 

203 

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

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

205 
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

206 
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

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

208 

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

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

13498  212 

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

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

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

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

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

220 
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

221 
*) 
13498  222 

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

227 
 GREATER => y; 

228 

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

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

233 
 GREATER => x; 

13498  234 

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

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

236 
val ratrelmax = foldr1 ratrelmax2; 
13498  237 

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

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

244 

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

246 

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

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

251 
else if not d then 

252 
if ord = GREATER 

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

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

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

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

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

261 
end; 

13498  262 

22950  263 
fun findex1 discr (v, lineqs) ex = 
264 
let 

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

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

272 
fun elim1 v x = 

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

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

13498  279 

280 
(* The base case: 

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

282 
fun pick_vars discr (ineqs,ex) = 

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

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

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

290 
val minmax = 
17951  291 
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

292 
else ratexact true o ratrelmax 
17951  293 
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

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

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

299 
in pick_vars discr (ineqs',ex') end 
13498  300 
end; 
301 

302 
fun findex0 discr n lineqs = 

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

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

308 
(*  *) 

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

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

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

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

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

315 

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

316 
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

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

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

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

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

321 

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

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

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

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

325 

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

326 
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

327 
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

328 
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

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

331 

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

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

333 
(* Add together (in)equations. *) 
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 

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

338 
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

339 

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

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

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

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

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

344 

49387  345 
fun elim_var v (i1 as Lineq(_,ty1,l1,_)) (i2 as Lineq(_,ty2,l2,_)) = 
23063  346 
let val c1 = nth l1 v and c2 = nth l2 v 
23261  347 
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

348 
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

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

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

351 
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

352 
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

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

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

355 
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

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

357 
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

358 

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

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

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

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

363 
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

364 

38052  365 
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

366 
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

367 

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

368 
fun calc_blowup l = 
33317  369 
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

370 
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

371 

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

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

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

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

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

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

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

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

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

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

383 

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

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

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

386 
fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys 
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
46709
diff
changeset

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

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

389 

44654  390 
fun print_ineqs ctxt ineqs = 
391 
if Config.get ctxt LA_Data.trace then 

12262  392 
tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset

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

395 
commas(map string_of_int l)) ineqs)) 
9073  396 
else (); 
6056  397 

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

400 

44654  401 
fun elim ctxt (ineqs, hist) = 
402 
let val _ = print_ineqs ctxt ineqs 

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

403 
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

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

405 
then case Library.find_first is_contradictory triv of 
44654  406 
NONE => elim ctxt (nontriv, hist) 
15531  407 
 SOME(Lineq(_,_,_,j)) => Success j 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

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

411 
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

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

413 
let val c = 
33042  414 
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

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

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

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

418 
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

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

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

423 
val others = map (elim_var v eq) roth @ ioth 
44654  424 
in elim ctxt (others,(v,nontriv)::hist) end 
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

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

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

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

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

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

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

44654  437 
in elim ctxt (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

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

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

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

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

443 
(* Translate back a proof. *) 
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 

44654  446 
fun trace_thm ctxt msgs th = 
447 
(if Config.get ctxt LA_Data.trace 

448 
then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th])) 

449 
else (); th); 

9073  450 

44654  451 
fun trace_term ctxt msgs t = 
452 
(if Config.get ctxt LA_Data.trace 

453 
then tracing (cat_lines (msgs @ [Syntax.string_of_term ctxt t])) 

454 
else (); t); 

24076  455 

44654  456 
fun trace_msg ctxt msg = 
457 
if Config.get ctxt LA_Data.trace then tracing msg else (); 

9073  458 

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

461 

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

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

463 
union_term (map fst lhs) o union_term (map fst rhs); 
6056  464 

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

465 
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

466 

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

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

470 
with 0 <= n. 

471 
*) 

472 
local 

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

475 

24076  476 
fun mkthm ss asms (just: injust) = 
477 
let 

478 
val ctxt = Simplifier.the_context ss; 

42361  479 
val thy = Proof_Context.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

480 
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

481 
val number_of = number_of ctxt; 
24076  482 
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

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

484 
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

485 
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

486 

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

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

488 
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

489 

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

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

491 
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

492 
fun try_add thms thm = get_first (fn th => add2 th thm) thms; 
6056  493 

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

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

495 
(case add2 thm1 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 
(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

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

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

500 
handle Option => 
44654  501 
(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

502 
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

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

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

505 

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

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

507 
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

508 
in mul n thm end; 
10575  509 

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

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

511 
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

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

513 
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

514 
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

515 
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

516 

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

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

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

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

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

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

522 
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

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

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

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

526 
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

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

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

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

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

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

532 
end); 
10691  533 

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

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

535 
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

536 
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

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

538 

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

539 
fun simp thm = 
44654  540 
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

541 
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end; 
6056  542 

44654  543 
fun mk (Asm i) = trace_thm ctxt ["Asm " ^ string_of_int i] (nth asms i) 
544 
 mk (Nat i) = trace_thm ctxt ["Nat " ^ string_of_int i] (LA_Logic.mk_nat_thm thy (nth atoms i)) 

545 
 mk (LessD j) = trace_thm ctxt ["L"] (hd ([mk j] RL lessD)) 

546 
 mk (NotLeD j) = trace_thm ctxt ["NLe"] (mk j RS LA_Logic.not_leD) 

547 
 mk (NotLeDD j) = trace_thm ctxt ["NLeD"] (hd ([mk j RS LA_Logic.not_leD] RL lessD)) 

548 
 mk (NotLessD j) = trace_thm ctxt ["NL"] (mk j RS LA_Logic.not_lessD) 

549 
 mk (Added (j1, j2)) = simp (trace_thm ctxt ["+"] (add_thms (mk j1) (mk j2))) 

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

550 
 mk (Multiplied (n, j)) = 
44654  551 
(trace_msg ctxt ("*" ^ 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

552 

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

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

554 
let 
44654  555 
val _ = trace_msg ctxt "mkthm"; 
556 
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

557 
val fls = simplify simpset' thm; 
44654  558 
val _ = trace_thm ctxt ["After simplification:"] fls; 
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset

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

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

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

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

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

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

565 
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

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

567 
in fls end 
44654  568 
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

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

570 

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

572 

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

574 
AList.lookup Pattern.aeconv poly atom > the_default 0; 
10691  575 

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

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

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

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

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

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

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

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

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

595 
 "~<=" => if discrete 

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

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

598 
 "<" => if discrete 

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

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

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

602 
 "=" => 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

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

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

605 

13498  606 
(*  *) 
607 
(* Print (counter) example *) 

608 
(*  *) 

609 

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

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

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

614 
else string_of_int p ^ "/" ^ string_of_int q 
13498  615 
in a ^ " = " ^ s end; 
616 

43607
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

617 
fun is_variable (Free _) = true 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

618 
 is_variable (Var _) = true 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

619 
 is_variable (Bound _) = true 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

620 
 is_variable _ = false 
13498  621 

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

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

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

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

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

22950  631 
else (hist, replicate n Rat.zero) 
43607
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

632 
val produce_ex = 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

633 
map print_atom #> commas #> 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

634 
prefix "Counterexample (possibly spurious):\n" 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

635 
val ex = ( 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

636 
uncurry (fold (findex1 discr)) start 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

637 
> map2 pair (atoms ~~ discr) 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

638 
> filter (fn ((t, _), _) => is_variable t) 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

639 
> map (apfst (apfst show_term)) 
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset

640 
> (fn [] => NONE  sdss => SOME (produce_ex sdss))) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset

641 
handle NoEx => NONE 
24076  642 
in 
643 
case ex of 

44654  644 
SOME s => 
645 
(warning "Linear arithmetic failed  see trace for a (potentially spurious) counterexample."; 

646 
tracing s) 

30687  647 
 NONE => warning "Linear arithmetic failed" 
24076  648 
end; 
13498  649 

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

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

651 

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

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

655 
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

656 
else NONE; 
6056  657 

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

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

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

663 
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

664 
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

665 
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

666 
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

667 

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

668 
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

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

670 

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

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

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

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

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

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

676 

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

677 
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

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

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

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

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

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

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

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

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

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

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

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

693 
 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

694 
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

695 
 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

696 
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

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

698 
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

699 
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

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

701 
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

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

703 
ineqs > elim_neq' true 
26945  704 
> 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

705 
end 
13464  706 

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

707 
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

708 
 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

709 
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

710 

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

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

712 
 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

713 
 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

714 

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

715 
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

716 
> (* userdefined preprocessing of the subgoal *) 
24076  717 
(if do_pre then LA_Data.pre_decomp ctxt else Library.single) 
44654  718 
> tap (fn subgoals => trace_msg ctxt ("Preprocessing yields " ^ 
23195  719 
string_of_int (length subgoals) ^ " subgoal(s) total.")) 
22846  720 
> (* produce the internal encoding of (in)equalities *) 
24076  721 
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

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

723 
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

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

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

727 
map (apsnd (number_hyps 0)) 
23195  728 
in 
44654  729 
trace_msg ctxt ("Splitting of inequalities yields " ^ 
23195  730 
string_of_int (length result) ^ " subgoal(s) total."); 
731 
result 

732 
end; 

13464  733 

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

735 
union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); 
13498  736 

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

739 

24076  740 
fun refutes ctxt params show_ex : 
26945  741 
(typ list * (LA_Data.decomp * int) list) list > injust list > injust list option = 
742 
let 

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

744 
let 

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

745 
val atoms = atoms_of (map fst initems) 
26945  746 
val n = length atoms 
38052  747 
val mkleq = mklineq atoms 
26945  748 
val ixs = 0 upto (n  1) 
749 
val iatoms = atoms ~~ ixs 

32952  750 
val natlineqs = map_filter (mknat Ts ixs) iatoms 
26945  751 
val ineqs = map mkleq initems @ natlineqs 
44654  752 
in case elim ctxt (ineqs, []) of 
26945  753 
Success j => 
44654  754 
(trace_msg ctxt ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); 
26945  755 
refute initemss (js @ [j])) 
756 
 Failure hist => 

44654  757 
(if not show_ex orelse not (Config.get ctxt LA_Data.verbose) then () 
26945  758 
else 
759 
let 

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

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

43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42361
diff
changeset

762 
(Name.invent (Variable.names_of ctxt') Name.uu (length Ts  length params)) 
26945  763 
val params' = (more_names @ param_names) ~~ Ts 
764 
in 

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

766 
end; NONE) 

767 
end 

768 
 refute [] js = SOME js 

769 
in refute end; 

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

770 

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

771 
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

772 
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

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

774 

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

776 

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

777 
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

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

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

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

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

783 
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

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

785 
 is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") 
44654  786 
val neq_limit = Config.get ctxt LA_Data.neq_limit 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

787 
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

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

789 
if split_neq then () 
24076  790 
else 
44654  791 
trace_msg ctxt ("neq_limit exceeded (current value is " ^ 
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset

792 
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

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

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

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

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

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

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

801 

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

802 
fun refute_tac ss (i, split_neq, justs) = 
6074  803 
fn state => 
24076  804 
let 
805 
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

806 
val _ = trace_thm ctxt 
44654  807 
["refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ 
808 
string_of_int (length justs) ^ " justification(s)):"] state 

24076  809 
val {neqE, ...} = get_data ctxt; 
810 
fun just1 j = 

811 
(* eliminate inequalities *) 

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

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

813 
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

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

815 
all_tac) THEN 
44654  816 
PRIMITIVE (trace_thm ctxt ["State after neqE:"]) THEN 
24076  817 
(* use theorems generated from the actual justifications *) 
32283  818 
Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i 
24076  819 
in 
820 
(* rewrite "[ A1; ...; An ] ==> B" to "[ A1; ...; An; ~B ] ==> False" *) 

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

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

823 
DETERM (LA_Data.pre_tac ss i) THEN 
44654  824 
PRIMITIVE (trace_thm ctxt ["State after pre_tac:"]) THEN 
24076  825 
(* prove every resulting subgoal, using its justification *) 
826 
EVERY (map just1 justs) 

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

827 
end state; 
6074  828 

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

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

830 
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

831 
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

832 
*) 
24076  833 
fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => 
834 
let 

835 
val ctxt = Simplifier.the_context ss 

836 
val params = rev (Logic.strip_params A) 

837 
val Hs = Logic.strip_assums_hyp A 

838 
val concl = Logic.strip_assums_concl A 

44654  839 
val _ = trace_term ctxt ["Trying to refute subgoal " ^ string_of_int i] A 
24076  840 
in 
841 
case prove ctxt params show_ex true Hs concl of 

44654  842 
(_, NONE) => (trace_msg ctxt "Refutation failed."; no_tac) 
843 
 (split_neq, SOME js) => (trace_msg ctxt "Refutation succeeded."; 

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

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

846 

46709
65a9b30bff00
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
wenzelm
parents:
44654
diff
changeset

847 
fun prems_lin_arith_tac ss = 
65a9b30bff00
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
wenzelm
parents:
44654
diff
changeset

848 
Method.insert_tac (Simplifier.prems_of ss) THEN' 
24076  849 
simpset_lin_arith_tac ss false; 
17613  850 

24076  851 
fun lin_arith_tac ctxt = 
852 
simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); 

853 

854 

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

855 

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

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

857 

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

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

859 
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

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

861 

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

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

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

864 

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

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

866 

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

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

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

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

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

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

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

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

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

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

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

877 

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

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

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

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

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

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

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

886 
let val (ct1, ct2) = extract (cprop_of spl) 
36945  887 
val thm1 = Thm.assume ct1 
888 
val thm2 = Thm.assume ct2 

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

889 
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

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

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

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

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

894 

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

897 
let 

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

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

36945  900 
val thm1' = Thm.implies_intr ct1 thm1 
901 
val thm2' = Thm.implies_intr ct2 thm2 

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

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

904 

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

905 
fun prover ss thms Tconcl (js : injust list) split_neq pos : thm option = 
24076  906 
let 
907 
val ctxt = Simplifier.the_context ss 

42361  908 
val thy = Proof_Context.theory_of ctxt 
24076  909 
val nTconcl = LA_Logic.neg_prop Tconcl 
910 
val cnTconcl = cterm_of thy nTconcl 

36945  911 
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

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

36945  915 
val concl = Thm.implies_intr cnTconcl Falsethm COMP contr 
44654  916 
in SOME (trace_thm ctxt ["Proved by lin. arith. prover:"] (LA_Logic.mk_Eq concl)) end 
24076  917 
(*in case concl contains ?var, which makes assume fail:*) (* FIXME Variable.import_terms *) 
918 
handle THM _ => NONE; 

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

919 

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

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

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

924 
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

925 
*) 
24076  926 
fun lin_arith_simproc ss concl = 
927 
let 

928 
val ctxt = Simplifier.the_context ss 

43597  929 
val thms = maps LA_Logic.atomize (Simplifier.prems_of ss) 
24076  930 
val Hs = map Thm.prop_of thms 
6102  931 
val Tconcl = LA_Logic.mk_Trueprop concl 
24076  932 
in 
933 
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

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

935 
 (_, NONE) => 
24076  936 
let val nTconcl = LA_Logic.neg_prop Tconcl in 
937 
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

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

939 
 (_, NONE) => NONE 
24076  940 
end 
941 
end; 

6074  942 

943 
end; 