author  wenzelm 
Sat, 08 Jul 2006 12:54:41 +0200  
changeset 20053  7f32ce6354d6 
parent 19277  f7602e74d948 
child 20194  c9dbce9a23a1 
permissions  rwrr 
13876  1 
(* Title: HOL/Integ/presburger.ML 
2 
ID: $Id$ 

3 
Author: Amine Chaieb and Stefan Berghofer, TU Muenchen 

4 

17465  5 
Tactic for solving arithmetical Goals in Presburger Arithmetic. 
13876  6 

17465  7 
This version of presburger deals with occurences of functional symbols 
8 
in the subgoal and abstract over them to try to prove the more general 

9 
formula. It then resolves with the subgoal. To enable this feature 

10 
call the procedure with the parameter abs. 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

11 
*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

12 

13876  13 
signature PRESBURGER = 
14 
sig 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

15 
val presburger_tac : bool > bool > int > tactic 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

16 
val presburger_method : bool > bool > int > Proof.method 
18708  17 
val setup : theory > theory 
13876  18 
val trace : bool ref 
19 
end; 

20 

21 
structure Presburger: PRESBURGER = 

22 
struct 

23 

24 
val trace = ref false; 

25 
fun trace_msg s = if !trace then tracing s else (); 

26 

27 
(**) 

28 
(*cooper_pp: provefunction for the oneexstance quantifier elimination*) 

29 
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*) 

30 
(**) 

31 

14941  32 

20053  33 
val presburger_ss = simpset (); 
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

34 
val binarith = map thm 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

35 
["Pls_0_eq", "Min_1_eq", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

36 
"bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

37 
"bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

38 
"bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

39 
"bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

40 
"bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

41 
"bin_add_Pls_right", "bin_add_Min_right"]; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

42 
val intarithrel = 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

43 
(map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

44 
"int_le_number_of_eq","int_iszero_number_of_0", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

45 
"int_less_number_of_eq_neg"]) @ 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

46 
(map (fn s => thm s RS thm "lift_bool") 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

47 
["int_iszero_number_of_Pls","int_iszero_number_of_1", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

48 
"int_neg_number_of_Min"])@ 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

49 
(map (fn s => thm s RS thm "nlift_bool") 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

50 
["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]); 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

51 

46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

52 
val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

53 
"int_number_of_diff_sym", "int_number_of_mult_sym"]; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

54 
val natarith = map thm ["add_nat_number_of", "diff_nat_number_of", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

55 
"mult_nat_number_of", "eq_nat_number_of", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

56 
"less_nat_number_of"] 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

57 
val powerarith = 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

58 
(map thm ["nat_number_of", "zpower_number_of_even", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

59 
"zpower_Pls", "zpower_Min"]) @ 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

60 
[(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

61 
thm "one_eq_Numeral1_nring"] 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

62 
(thm "zpower_number_of_odd"))] 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

63 

18393  64 
val comp_arith = binarith @ intarith @ intarithrel @ natarith 
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

65 
@ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; 
14801
2d27b5ebc447
 deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset

66 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

67 
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
13876  68 
let val (xn1,p1) = variant_abs (xn,xT,p) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

69 
in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end; 
13876  70 

71 
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm 

72 
(CooperProof.proof_of_evalc sg); 

73 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

74 
fun tmproof_of_int_qelim sg fm = 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

75 
Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel 
13876  76 
(CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm; 
77 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

78 

13876  79 
(* Theorems to be used in this tactic*) 
80 

81 
val zdvd_int = thm "zdvd_int"; 

82 
val zdiff_int_split = thm "zdiff_int_split"; 

83 
val all_nat = thm "all_nat"; 

84 
val ex_nat = thm "ex_nat"; 

85 
val number_of1 = thm "number_of1"; 

86 
val number_of2 = thm "number_of2"; 

87 
val split_zdiv = thm "split_zdiv"; 

88 
val split_zmod = thm "split_zmod"; 

89 
val mod_div_equality' = thm "mod_div_equality'"; 

90 
val split_div' = thm "split_div'"; 

91 
val Suc_plus1 = thm "Suc_plus1"; 

92 
val imp_le_cong = thm "imp_le_cong"; 

93 
val conj_le_cong = thm "conj_le_cong"; 

18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

94 
val nat_mod_add_eq = mod_add1_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

95 
val nat_mod_add_left_eq = mod_add_left_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

96 
val nat_mod_add_right_eq = mod_add_right_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

97 
val int_mod_add_eq = zmod_zadd1_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

98 
val int_mod_add_left_eq = zmod_zadd_left_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

99 
val int_mod_add_right_eq = zmod_zadd_right_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

100 
val nat_div_add_eq = div_add1_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

101 
val int_div_add_eq = zdiv_zadd1_eq RS sym; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

102 
val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

103 
val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1; 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

104 

13876  105 

106 
(* extract all the constants in a term*) 

107 
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs 

108 
 add_term_typed_consts (t $ u, cs) = 

109 
add_term_typed_consts (t, add_term_typed_consts (u, cs)) 

110 
 add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs) 

111 
 add_term_typed_consts (_, cs) = cs; 

112 

113 
fun term_typed_consts t = add_term_typed_consts(t,[]); 

114 

15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15620
diff
changeset

115 
(* Some Types*) 
13876  116 
val bT = HOLogic.boolT; 
15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15574
diff
changeset

117 
val bitT = HOLogic.bitT; 
13876  118 
val iT = HOLogic.intT; 
119 
val binT = HOLogic.binT; 

120 
val nT = HOLogic.natT; 

121 

122 
(* Allowed Consts in formulae for presburger tactic*) 

123 

124 
val allowed_consts = 

125 
[("All", (iT > bT) > bT), 

126 
("Ex", (iT > bT) > bT), 

127 
("All", (nT > bT) > bT), 

128 
("Ex", (nT > bT) > bT), 

129 

130 
("op &", bT > bT > bT), 

131 
("op ", bT > bT > bT), 

132 
("op >", bT > bT > bT), 

133 
("op =", bT > bT > bT), 

134 
("Not", bT > bT), 

135 

19277  136 
("Orderings.less_eq", iT > iT > bT), 
13876  137 
("op =", iT > iT > bT), 
19277  138 
("Orderings.less", iT > iT > bT), 
13876  139 
("Divides.op dvd", iT > iT > bT), 
140 
("Divides.op div", iT > iT > iT), 

141 
("Divides.op mod", iT > iT > iT), 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

142 
("HOL.plus", iT > iT > iT), 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

143 
("HOL.minus", iT > iT > iT), 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

144 
("HOL.times", iT > iT > iT), 
13876  145 
("HOL.abs", iT > iT), 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

146 
("HOL.uminus", iT > iT), 
14801
2d27b5ebc447
 deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset

147 
("HOL.max", iT > iT > iT), 
2d27b5ebc447
 deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset

148 
("HOL.min", iT > iT > iT), 
13876  149 

19277  150 
("Orderings.less_eq", nT > nT > bT), 
13876  151 
("op =", nT > nT > bT), 
19277  152 
("Orderings.less", nT > nT > bT), 
13876  153 
("Divides.op dvd", nT > nT > bT), 
154 
("Divides.op div", nT > nT > nT), 

155 
("Divides.op mod", nT > nT > nT), 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

156 
("HOL.plus", nT > nT > nT), 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

157 
("HOL.minus", nT > nT > nT), 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18708
diff
changeset

158 
("HOL.times", nT > nT > nT), 
13876  159 
("Suc", nT > nT), 
14801
2d27b5ebc447
 deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset

160 
("HOL.max", nT > nT > nT), 
2d27b5ebc447
 deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset

161 
("HOL.min", nT > nT > nT), 
13876  162 

15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15574
diff
changeset

163 
("Numeral.bit.B0", bitT), 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15574
diff
changeset

164 
("Numeral.bit.B1", bitT), 
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15574
diff
changeset

165 
("Numeral.Bit", binT > bitT > binT), 
15013  166 
("Numeral.Pls", binT), 
167 
("Numeral.Min", binT), 

13876  168 
("Numeral.number_of", binT > iT), 
169 
("Numeral.number_of", binT > nT), 

170 
("0", nT), 

171 
("0", iT), 

172 
("1", nT), 

173 
("1", iT), 

174 
("False", bT), 

175 
("True", bT)]; 

176 

177 
(* Preparation of the formula to be sent to the Integer quantifier *) 

178 
(* elimination procedure *) 

179 
(* Transforms meta implications and meta quantifiers to object *) 

180 
(* implications and object quantifiers *) 

181 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

182 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

183 
(*==================================*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

184 
(* Abstracting on subterms ========*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

185 
(*==================================*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

186 
(* Returns occurences of terms that are function application of type int or nat*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

187 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

188 
fun getfuncs fm = case strip_comb fm of 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

189 
(Free (_, T), ts as _ :: _) => 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

190 
if body_type T mem [iT, nT] 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

191 
andalso not (ts = []) andalso forall (null o loose_bnos) ts 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

192 
then [fm] 
15570  193 
else Library.foldl op union ([], map getfuncs ts) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

194 
 (Var (_, T), ts as _ :: _) => 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

195 
if body_type T mem [iT, nT] 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

196 
andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm] 
15570  197 
else Library.foldl op union ([], map getfuncs ts) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

198 
 (Const (s, T), ts) => 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

199 
if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT]) 
15570  200 
then Library.foldl op union ([], map getfuncs ts) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

201 
else [fm] 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

202 
 (Abs (s, T, t), _) => getfuncs t 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

203 
 _ => []; 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

204 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

205 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

206 
fun abstract_pres sg fm = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

207 
foldr (fn (t, u) => 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

208 
let val T = fastype_of t 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

209 
in all T $ Abs ("x", T, abstract_over (t, u)) end) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

210 
fm (getfuncs fm); 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

211 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

212 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

213 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

214 
(* hasfuncs_on_bounds dont care of the type of the functions applied! 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

215 
It returns true if there is a subterm coresponding to the application of 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

216 
a function on a bounded variable. 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

217 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

218 
Function applications are allowed only for well predefined functions a 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

219 
consts*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

220 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

221 
fun has_free_funcs fm = case strip_comb fm of 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

222 
(Free (_, T), ts as _ :: _) => 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

223 
if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT])) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

224 
then true 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

225 
else exists (fn x => x) (map has_free_funcs ts) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

226 
 (Var (_, T), ts as _ :: _) => 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

227 
if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT]) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

228 
then true 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

229 
else exists (fn x => x) (map has_free_funcs ts) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

230 
 (Const (s, T), ts) => exists (fn x => x) (map has_free_funcs ts) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

231 
 (Abs (s, T, t), _) => has_free_funcs t 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

232 
_ => false; 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

233 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

234 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

235 
(*returns true if the formula is relevant for presburger arithmetic tactic 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

236 
The constants occuring in term t should be a subset of the allowed_consts 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

237 
There also should be no occurences of application of functions on bounded 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

238 
variables. Whenever this function will be used, it will be ensured that t 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

239 
will not contain subterms with function symbols that could have been 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

240 
abstracted over.*) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

241 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

242 
fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
15570  243 
map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @ 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

244 
map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

245 
subset [iT, nT] 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

246 
andalso not (has_free_funcs t); 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

247 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

248 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

249 
fun prepare_for_presburger sg q fm = 
13876  250 
let 
251 
val ps = Logic.strip_params fm 

252 
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) 

253 
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

254 
val _ = if relevant (rev ps) c then () 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

255 
else (trace_msg ("Conclusion is not a presburger term:\n" ^ 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

256 
Sign.string_of_term sg c); raise CooperDec.COOPER) 
13876  257 
fun mk_all ((s, T), (P,n)) = 
258 
if 0 mem loose_bnos P then 

259 
(HOLogic.all_const T $ Abs (s, T, P), n) 

260 
else (incr_boundvars ~1 P, n1) 

261 
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; 

15570  262 
val (rhs,irhs) = List.partition (relevant (rev ps)) hs 
13876  263 
val np = length ps 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

264 
val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

265 
(foldr HOLogic.mk_imp c rhs, np) ps 
15570  266 
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT) 
13876  267 
(term_frees fm' @ term_vars fm'); 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

268 
val fm2 = foldr mk_all2 fm' vs 
13876  269 
in (fm2, np + length vs, length rhs) end; 
270 

271 
(*Object quantifier to meta *) 

272 
fun spec_step n th = if (n=0) then th else (spec_step (n1) th) RS spec ; 

273 

274 
(* object implication to meta*) 

275 
fun mp_step n th = if (n=0) then th else (mp_step (n1) th) RS mp; 

276 

277 
(* the presburger tactic*) 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

278 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

279 
(* Parameters : q = flag for quantify ofer free variables ; 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

280 
a = flag for abstracting over function occurences 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

281 
i = subgoal *) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

282 

af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

283 
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st => 
13876  284 
let 
17465  285 
val g = List.nth (prems_of st, i  1) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

286 
val sg = sign_of_thm st 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

287 
(* The Abstraction step *) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

288 
val g' = if a then abstract_pres sg g else g 
13876  289 
(* Transform the term*) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

290 
val (t,np,nh) = prepare_for_presburger sg q g' 
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15620
diff
changeset

291 
(* Some simpsets for dealing with mod div abs and nat*) 
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

292 
val mod_div_simpset = HOL_basic_ss 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

293 
addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

294 
nat_mod_add_right_eq, int_mod_add_eq, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

295 
int_mod_add_right_eq, int_mod_add_left_eq, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

296 
nat_div_add_eq, int_div_add_eq, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

297 
mod_self, zmod_self, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

298 
DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

299 
ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV, 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

300 
zdiv_zero,zmod_zero,div_0,mod_0, 
18393  301 
zdiv_1,zmod_1,div_1,mod_1, 
302 
Suc_plus1] 

18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

303 
addsimps add_ac 
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

304 
addsimprocs [cancel_div_mod_proc] 
13876  305 
val simpset0 = HOL_basic_ss 
306 
addsimps [mod_div_equality', Suc_plus1] 

18393  307 
addsimps comp_arith 
13997  308 
addsplits [split_zdiv, split_zmod, split_div', split_min, split_max] 
13876  309 
(* Simp rules for changing (n::int) to int n *) 
310 
val simpset1 = HOL_basic_ss 

311 
addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) 

312 
[int_int_eq, zle_int, zless_int, zadd_int, zmult_int] 

313 
addsplits [zdiff_int_split] 

314 
(*simp rules for elimination of int n*) 

315 

316 
val simpset2 = HOL_basic_ss 

317 
addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1] 

318 
addcongs [conj_le_cong, imp_le_cong] 

319 
(* simp rules for elimination of abs *) 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14130
diff
changeset

320 
val simpset3 = HOL_basic_ss addsplits [abs_split] 
13876  321 
val ct = cterm_of sg (HOLogic.mk_Trueprop t) 
322 
(* Theorem for the nat > int transformation *) 

323 
val pre_thm = Seq.hd (EVERY 

18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
18155
diff
changeset

324 
[simp_tac mod_div_simpset 1, simp_tac simpset0 1, 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

325 
TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), 
14801
2d27b5ebc447
 deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents:
14758
diff
changeset

326 
TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)] 
13876  327 
(trivial ct)) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

328 
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) 
13876  329 
(* The result of the quantifier elimination *) 
330 
val (th, tac) = case (prop_of pre_thm) of 

331 
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => 

14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

332 
let val pth = 
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

333 
(* If quick_and_dirty then run without proof generation as oracle*) 
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

334 
if !quick_and_dirty 
16836  335 
then presburger_oracle sg (Pattern.eta_long [] t1) 
14941  336 
(* 
337 
assume (cterm_of sg 

14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

338 
(HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) 
14941  339 
*) 
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

340 
else tmproof_of_int_qelim sg (Pattern.eta_long [] t1) 
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

341 
in 
13876  342 
(trace_msg ("calling procedure with term:\n" ^ 
343 
Sign.string_of_term sg t1); 

14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

344 
((pth RS iffD2) RS pre_thm, 
13876  345 
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) 
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14882
diff
changeset

346 
end 
13876  347 
 _ => (pre_thm, assm_tac i) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

348 
in (rtac (((mp_step nh) o (spec_step np)) th) i 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

349 
THEN tac) st 
14130  350 
end handle Subscript => no_tac st  CooperDec.COOPER => no_tac st); 
13876  351 

352 
fun presburger_args meth = 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

353 
let val parse_flag = 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

354 
Args.$$$ "no_quantify" >> K (apfst (K false)) 
18155
e5ab63ca6b0f
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
chaieb
parents:
17465
diff
changeset

355 
 Args.$$$ "no_abs" >> K (apsnd (K false)); 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

356 
in 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

357 
Method.simple_args 
14882  358 
(Scan.optional (Args.$$$ "("  Scan.repeat1 parse_flag  Args.$$$ ")") [] >> 
18155
e5ab63ca6b0f
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
chaieb
parents:
17465
diff
changeset

359 
curry (Library.foldl op >) (true, true)) 
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

360 
(fn (q,a) => fn _ => meth q a 1) 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

361 
end; 
13876  362 

14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

363 
fun presburger_method q a i = Method.METHOD (fn facts => 
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset

364 
Method.insert_tac facts 1 THEN presburger_tac q a i) 
13876  365 

366 
val setup = 

18708  367 
Method.add_method ("presburger", 
368 
presburger_args presburger_method, 

369 
"decision procedure for Presburger arithmetic") #> 

370 
ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} => 

371 
{splits = splits, inj_consts = inj_consts, discrete = discrete, 

372 
presburger = SOME (presburger_tac true true)}); 

13876  373 

374 
end; 

375 

18155
e5ab63ca6b0f
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
chaieb
parents:
17465
diff
changeset

376 
val presburger_tac = Presburger.presburger_tac true true; 