src/HOL/Integ/presburger.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18393 af72cbfa00a5
child 19233 77ca20b0ed77
permissions -rw-r--r--
setup: theory -> theory;
berghofe@13876
     1
(*  Title:      HOL/Integ/presburger.ML
berghofe@13876
     2
    ID:         $Id$
berghofe@13876
     3
    Author:     Amine Chaieb and Stefan Berghofer, TU Muenchen
berghofe@13876
     4
wenzelm@17465
     5
Tactic for solving arithmetical Goals in Presburger Arithmetic.
berghofe@13876
     6
wenzelm@17465
     7
This version of presburger deals with occurences of functional symbols
wenzelm@17465
     8
in the subgoal and abstract over them to try to prove the more general
wenzelm@17465
     9
formula. It then resolves with the subgoal. To enable this feature
wenzelm@17465
    10
call the procedure with the parameter abs.
chaieb@14758
    11
*)
chaieb@14758
    12
berghofe@13876
    13
signature PRESBURGER = 
berghofe@13876
    14
sig
chaieb@14758
    15
 val presburger_tac : bool -> bool -> int -> tactic
chaieb@14758
    16
 val presburger_method : bool -> bool -> int -> Proof.method
wenzelm@18708
    17
 val setup : theory -> theory
berghofe@13876
    18
 val trace : bool ref
berghofe@13876
    19
end;
berghofe@13876
    20
berghofe@13876
    21
structure Presburger: PRESBURGER =
berghofe@13876
    22
struct
berghofe@13876
    23
berghofe@13876
    24
val trace = ref false;
berghofe@13876
    25
fun trace_msg s = if !trace then tracing s else ();
berghofe@13876
    26
berghofe@13876
    27
(*-----------------------------------------------------------------*)
berghofe@13876
    28
(*cooper_pp: provefunction for the one-exstance quantifier elimination*)
berghofe@13876
    29
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
berghofe@13876
    30
(*-----------------------------------------------------------------*)
berghofe@13876
    31
chaieb@14941
    32
berghofe@14801
    33
val presburger_ss = simpset_of (theory "Presburger");
chaieb@18202
    34
val binarith = map thm
chaieb@18202
    35
  ["Pls_0_eq", "Min_1_eq",
chaieb@18202
    36
 "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
chaieb@18202
    37
  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
chaieb@18202
    38
  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
chaieb@18202
    39
  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
chaieb@18202
    40
  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
chaieb@18202
    41
  "bin_add_Pls_right", "bin_add_Min_right"];
chaieb@18202
    42
 val intarithrel = 
chaieb@18202
    43
     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
chaieb@18202
    44
		"int_le_number_of_eq","int_iszero_number_of_0",
chaieb@18202
    45
		"int_less_number_of_eq_neg"]) @
chaieb@18202
    46
     (map (fn s => thm s RS thm "lift_bool") 
chaieb@18202
    47
	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
chaieb@18202
    48
	   "int_neg_number_of_Min"])@
chaieb@18202
    49
     (map (fn s => thm s RS thm "nlift_bool") 
chaieb@18202
    50
	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
chaieb@18202
    51
     
chaieb@18202
    52
val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
chaieb@18202
    53
			"int_number_of_diff_sym", "int_number_of_mult_sym"];
chaieb@18202
    54
val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
chaieb@18202
    55
			"mult_nat_number_of", "eq_nat_number_of",
chaieb@18202
    56
			"less_nat_number_of"]
chaieb@18202
    57
val powerarith = 
chaieb@18202
    58
    (map thm ["nat_number_of", "zpower_number_of_even", 
chaieb@18202
    59
	      "zpower_Pls", "zpower_Min"]) @ 
chaieb@18202
    60
    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
chaieb@18202
    61
			   thm "one_eq_Numeral1_nring"] 
chaieb@18202
    62
  (thm "zpower_number_of_odd"))]
chaieb@18202
    63
chaieb@18393
    64
val comp_arith = binarith @ intarith @ intarithrel @ natarith 
chaieb@18202
    65
	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
berghofe@14801
    66
chaieb@14758
    67
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
berghofe@13876
    68
  let val (xn1,p1) = variant_abs (xn,xT,p)
chaieb@14758
    69
  in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
berghofe@13876
    70
berghofe@13876
    71
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
berghofe@13876
    72
  (CooperProof.proof_of_evalc sg);
berghofe@13876
    73
chaieb@14758
    74
fun tmproof_of_int_qelim sg fm =
chaieb@14758
    75
  Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
berghofe@13876
    76
    (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
berghofe@13876
    77
chaieb@14758
    78
berghofe@13876
    79
(* Theorems to be used in this tactic*)
berghofe@13876
    80
berghofe@13876
    81
val zdvd_int = thm "zdvd_int";
berghofe@13876
    82
val zdiff_int_split = thm "zdiff_int_split";
berghofe@13876
    83
val all_nat = thm "all_nat";
berghofe@13876
    84
val ex_nat = thm "ex_nat";
berghofe@13876
    85
val number_of1 = thm "number_of1";
berghofe@13876
    86
val number_of2 = thm "number_of2";
berghofe@13876
    87
val split_zdiv = thm "split_zdiv";
berghofe@13876
    88
val split_zmod = thm "split_zmod";
berghofe@13876
    89
val mod_div_equality' = thm "mod_div_equality'";
berghofe@13876
    90
val split_div' = thm "split_div'";
berghofe@13876
    91
val Suc_plus1 = thm "Suc_plus1";
berghofe@13876
    92
val imp_le_cong = thm "imp_le_cong";
berghofe@13876
    93
val conj_le_cong = thm "conj_le_cong";
chaieb@18202
    94
val nat_mod_add_eq = mod_add1_eq RS sym;
chaieb@18202
    95
val nat_mod_add_left_eq = mod_add_left_eq RS sym;
chaieb@18202
    96
val nat_mod_add_right_eq = mod_add_right_eq RS sym;
chaieb@18202
    97
val int_mod_add_eq = zmod_zadd1_eq RS sym;
chaieb@18202
    98
val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
chaieb@18202
    99
val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
chaieb@18202
   100
val nat_div_add_eq = div_add1_eq RS sym;
chaieb@18202
   101
val int_div_add_eq = zdiv_zadd1_eq RS sym;
chaieb@18202
   102
val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
chaieb@18202
   103
val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
chaieb@18202
   104
berghofe@13876
   105
berghofe@13876
   106
(* extract all the constants in a term*)
berghofe@13876
   107
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
berghofe@13876
   108
  | add_term_typed_consts (t $ u, cs) =
berghofe@13876
   109
      add_term_typed_consts (t, add_term_typed_consts (u, cs))
berghofe@13876
   110
  | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
berghofe@13876
   111
  | add_term_typed_consts (_, cs) = cs;
berghofe@13876
   112
berghofe@13876
   113
fun term_typed_consts t = add_term_typed_consts(t,[]);
berghofe@13876
   114
wenzelm@15661
   115
(* Some Types*)
berghofe@13876
   116
val bT = HOLogic.boolT;
paulson@15620
   117
val bitT = HOLogic.bitT;
berghofe@13876
   118
val iT = HOLogic.intT;
berghofe@13876
   119
val binT = HOLogic.binT;
berghofe@13876
   120
val nT = HOLogic.natT;
berghofe@13876
   121
berghofe@13876
   122
(* Allowed Consts in formulae for presburger tactic*)
berghofe@13876
   123
berghofe@13876
   124
val allowed_consts =
berghofe@13876
   125
  [("All", (iT --> bT) --> bT),
berghofe@13876
   126
   ("Ex", (iT --> bT) --> bT),
berghofe@13876
   127
   ("All", (nT --> bT) --> bT),
berghofe@13876
   128
   ("Ex", (nT --> bT) --> bT),
berghofe@13876
   129
berghofe@13876
   130
   ("op &", bT --> bT --> bT),
berghofe@13876
   131
   ("op |", bT --> bT --> bT),
berghofe@13876
   132
   ("op -->", bT --> bT --> bT),
berghofe@13876
   133
   ("op =", bT --> bT --> bT),
berghofe@13876
   134
   ("Not", bT --> bT),
berghofe@13876
   135
berghofe@13876
   136
   ("op <=", iT --> iT --> bT),
berghofe@13876
   137
   ("op =", iT --> iT --> bT),
berghofe@13876
   138
   ("op <", iT --> iT --> bT),
berghofe@13876
   139
   ("Divides.op dvd", iT --> iT --> bT),
berghofe@13876
   140
   ("Divides.op div", iT --> iT --> iT),
berghofe@13876
   141
   ("Divides.op mod", iT --> iT --> iT),
berghofe@13876
   142
   ("op +", iT --> iT --> iT),
berghofe@13876
   143
   ("op -", iT --> iT --> iT),
berghofe@13876
   144
   ("op *", iT --> iT --> iT), 
berghofe@13876
   145
   ("HOL.abs", iT --> iT),
berghofe@13876
   146
   ("uminus", iT --> iT),
berghofe@14801
   147
   ("HOL.max", iT --> iT --> iT),
berghofe@14801
   148
   ("HOL.min", iT --> iT --> iT),
berghofe@13876
   149
berghofe@13876
   150
   ("op <=", nT --> nT --> bT),
berghofe@13876
   151
   ("op =", nT --> nT --> bT),
berghofe@13876
   152
   ("op <", nT --> nT --> bT),
berghofe@13876
   153
   ("Divides.op dvd", nT --> nT --> bT),
berghofe@13876
   154
   ("Divides.op div", nT --> nT --> nT),
berghofe@13876
   155
   ("Divides.op mod", nT --> nT --> nT),
berghofe@13876
   156
   ("op +", nT --> nT --> nT),
berghofe@13876
   157
   ("op -", nT --> nT --> nT),
berghofe@13876
   158
   ("op *", nT --> nT --> nT), 
berghofe@13876
   159
   ("Suc", nT --> nT),
berghofe@14801
   160
   ("HOL.max", nT --> nT --> nT),
berghofe@14801
   161
   ("HOL.min", nT --> nT --> nT),
berghofe@13876
   162
paulson@15620
   163
   ("Numeral.bit.B0", bitT),
paulson@15620
   164
   ("Numeral.bit.B1", bitT),
paulson@15620
   165
   ("Numeral.Bit", binT --> bitT --> binT),
paulson@15013
   166
   ("Numeral.Pls", binT),
paulson@15013
   167
   ("Numeral.Min", binT),
berghofe@13876
   168
   ("Numeral.number_of", binT --> iT),
berghofe@13876
   169
   ("Numeral.number_of", binT --> nT),
berghofe@13876
   170
   ("0", nT),
berghofe@13876
   171
   ("0", iT),
berghofe@13876
   172
   ("1", nT),
berghofe@13876
   173
   ("1", iT),
berghofe@13876
   174
   ("False", bT),
berghofe@13876
   175
   ("True", bT)];
berghofe@13876
   176
berghofe@13876
   177
(* Preparation of the formula to be sent to the Integer quantifier *)
berghofe@13876
   178
(* elimination procedure                                           *)
berghofe@13876
   179
(* Transforms meta implications and meta quantifiers to object     *)
berghofe@13876
   180
(* implications and object quantifiers                             *)
berghofe@13876
   181
chaieb@14758
   182
chaieb@14758
   183
(*==================================*)
chaieb@14758
   184
(* Abstracting on subterms  ========*)
chaieb@14758
   185
(*==================================*)
chaieb@14758
   186
(* Returns occurences of terms that are function application of type int or nat*)
chaieb@14758
   187
chaieb@14758
   188
fun getfuncs fm = case strip_comb fm of
chaieb@14758
   189
    (Free (_, T), ts as _ :: _) =>
chaieb@14758
   190
      if body_type T mem [iT, nT] 
chaieb@14758
   191
         andalso not (ts = []) andalso forall (null o loose_bnos) ts 
chaieb@14758
   192
      then [fm]
skalberg@15570
   193
      else Library.foldl op union ([], map getfuncs ts)
chaieb@14758
   194
  | (Var (_, T), ts as _ :: _) =>
chaieb@14758
   195
      if body_type T mem [iT, nT] 
chaieb@14758
   196
         andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
skalberg@15570
   197
      else Library.foldl op union ([], map getfuncs ts)
chaieb@14758
   198
  | (Const (s, T), ts) =>
chaieb@14758
   199
      if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
skalberg@15570
   200
      then Library.foldl op union ([], map getfuncs ts)
chaieb@14758
   201
      else [fm]
chaieb@14758
   202
  | (Abs (s, T, t), _) => getfuncs t
chaieb@14758
   203
  | _ => [];
chaieb@14758
   204
chaieb@14758
   205
chaieb@14758
   206
fun abstract_pres sg fm = 
skalberg@15574
   207
  foldr (fn (t, u) =>
chaieb@14758
   208
      let val T = fastype_of t
chaieb@14758
   209
      in all T $ Abs ("x", T, abstract_over (t, u)) end)
skalberg@15574
   210
         fm (getfuncs fm);
chaieb@14758
   211
chaieb@14758
   212
chaieb@14758
   213
chaieb@14758
   214
(* hasfuncs_on_bounds dont care of the type of the functions applied!
chaieb@14758
   215
 It returns true if there is a subterm coresponding to the application of
chaieb@14758
   216
 a function on a bounded variable.
chaieb@14758
   217
chaieb@14758
   218
 Function applications are allowed only for well predefined functions a 
chaieb@14758
   219
 consts*)
chaieb@14758
   220
chaieb@14758
   221
fun has_free_funcs fm  = case strip_comb fm of
chaieb@14758
   222
    (Free (_, T), ts as _ :: _) => 
chaieb@14758
   223
      if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
chaieb@14758
   224
      then true
chaieb@14758
   225
      else exists (fn x => x) (map has_free_funcs ts)
chaieb@14758
   226
  | (Var (_, T), ts as _ :: _) =>
chaieb@14758
   227
      if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
chaieb@14758
   228
      then true
chaieb@14758
   229
      else exists (fn x => x) (map has_free_funcs ts)
chaieb@14758
   230
  | (Const (s, T), ts) =>  exists (fn x => x) (map has_free_funcs ts)
chaieb@14758
   231
  | (Abs (s, T, t), _) => has_free_funcs t
chaieb@14758
   232
  |_ => false;
chaieb@14758
   233
chaieb@14758
   234
chaieb@14758
   235
(*returns true if the formula is relevant for presburger arithmetic tactic
chaieb@14758
   236
The constants occuring in term t should be a subset of the allowed_consts
chaieb@14758
   237
 There also should be no occurences of application of functions on bounded 
chaieb@14758
   238
 variables. Whenever this function will be used, it will be ensured that t 
chaieb@14758
   239
 will not contain subterms with function symbols that could have been 
chaieb@14758
   240
 abstracted over.*)
chaieb@14758
   241
 
chaieb@14758
   242
fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
skalberg@15570
   243
  map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
chaieb@14758
   244
  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
chaieb@14758
   245
  subset [iT, nT]
chaieb@14758
   246
  andalso not (has_free_funcs t);
chaieb@14758
   247
chaieb@14758
   248
chaieb@14758
   249
fun prepare_for_presburger sg q fm = 
berghofe@13876
   250
  let
berghofe@13876
   251
    val ps = Logic.strip_params fm
berghofe@13876
   252
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
berghofe@13876
   253
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
chaieb@14758
   254
    val _ = if relevant (rev ps) c then () 
chaieb@14758
   255
               else  (trace_msg ("Conclusion is not a presburger term:\n" ^
chaieb@14758
   256
             Sign.string_of_term sg c); raise CooperDec.COOPER)
berghofe@13876
   257
    fun mk_all ((s, T), (P,n)) =
berghofe@13876
   258
      if 0 mem loose_bnos P then
berghofe@13876
   259
        (HOLogic.all_const T $ Abs (s, T, P), n)
berghofe@13876
   260
      else (incr_boundvars ~1 P, n-1)
berghofe@13876
   261
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
skalberg@15570
   262
    val (rhs,irhs) = List.partition (relevant (rev ps)) hs
berghofe@13876
   263
    val np = length ps
skalberg@15574
   264
    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
skalberg@15574
   265
      (foldr HOLogic.mk_imp c rhs, np) ps
skalberg@15570
   266
    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
berghofe@13876
   267
      (term_frees fm' @ term_vars fm');
skalberg@15574
   268
    val fm2 = foldr mk_all2 fm' vs
berghofe@13876
   269
  in (fm2, np + length vs, length rhs) end;
berghofe@13876
   270
berghofe@13876
   271
(*Object quantifier to meta --*)
berghofe@13876
   272
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
berghofe@13876
   273
berghofe@13876
   274
(* object implication to meta---*)
berghofe@13876
   275
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
berghofe@13876
   276
berghofe@13876
   277
(* the presburger tactic*)
chaieb@14758
   278
chaieb@14758
   279
(* Parameters : q = flag for quantify ofer free variables ; 
chaieb@14758
   280
                a = flag for abstracting over function occurences
chaieb@14758
   281
                i = subgoal  *)
chaieb@14758
   282
chaieb@14758
   283
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
berghofe@13876
   284
  let
wenzelm@17465
   285
    val g = List.nth (prems_of st, i - 1)
chaieb@14758
   286
    val sg = sign_of_thm st
chaieb@14758
   287
    (* The Abstraction step *)
chaieb@14758
   288
    val g' = if a then abstract_pres sg g else g
berghofe@13876
   289
    (* Transform the term*)
chaieb@14758
   290
    val (t,np,nh) = prepare_for_presburger sg q g'
wenzelm@15661
   291
    (* Some simpsets for dealing with mod div abs and nat*)
chaieb@18202
   292
    val mod_div_simpset = HOL_basic_ss 
chaieb@18202
   293
			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
chaieb@18202
   294
				  nat_mod_add_right_eq, int_mod_add_eq, 
chaieb@18202
   295
				  int_mod_add_right_eq, int_mod_add_left_eq,
chaieb@18202
   296
				  nat_div_add_eq, int_div_add_eq,
chaieb@18202
   297
				  mod_self, zmod_self,
chaieb@18202
   298
				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
chaieb@18202
   299
				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
chaieb@18202
   300
				  zdiv_zero,zmod_zero,div_0,mod_0,
chaieb@18393
   301
				  zdiv_1,zmod_1,div_1,mod_1,
chaieb@18393
   302
				  Suc_plus1]
chaieb@18202
   303
			addsimps add_ac
chaieb@18202
   304
			addsimprocs [cancel_div_mod_proc]
berghofe@13876
   305
    val simpset0 = HOL_basic_ss
berghofe@13876
   306
      addsimps [mod_div_equality', Suc_plus1]
chaieb@18393
   307
      addsimps comp_arith
berghofe@13997
   308
      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
berghofe@13876
   309
    (* Simp rules for changing (n::int) to int n *)
berghofe@13876
   310
    val simpset1 = HOL_basic_ss
berghofe@13876
   311
      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
berghofe@13876
   312
        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
berghofe@13876
   313
      addsplits [zdiff_int_split]
berghofe@13876
   314
    (*simp rules for elimination of int n*)
berghofe@13876
   315
berghofe@13876
   316
    val simpset2 = HOL_basic_ss
berghofe@13876
   317
      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
berghofe@13876
   318
      addcongs [conj_le_cong, imp_le_cong]
berghofe@13876
   319
    (* simp rules for elimination of abs *)
paulson@14353
   320
    val simpset3 = HOL_basic_ss addsplits [abs_split]
berghofe@13876
   321
    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
berghofe@13876
   322
    (* Theorem for the nat --> int transformation *)
berghofe@13876
   323
    val pre_thm = Seq.hd (EVERY
chaieb@18202
   324
      [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
chaieb@14758
   325
       TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
berghofe@14801
   326
       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
berghofe@13876
   327
      (trivial ct))
chaieb@14758
   328
    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
berghofe@13876
   329
    (* The result of the quantifier elimination *)
berghofe@13876
   330
    val (th, tac) = case (prop_of pre_thm) of
berghofe@13876
   331
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
chaieb@14920
   332
    let val pth = 
chaieb@14920
   333
          (* If quick_and_dirty then run without proof generation as oracle*)
chaieb@14920
   334
             if !quick_and_dirty 
wenzelm@16836
   335
             then presburger_oracle sg (Pattern.eta_long [] t1)
chaieb@14941
   336
(*
chaieb@14941
   337
assume (cterm_of sg 
chaieb@14920
   338
	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
chaieb@14941
   339
*)
chaieb@14920
   340
	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
chaieb@14920
   341
    in 
berghofe@13876
   342
          (trace_msg ("calling procedure with term:\n" ^
berghofe@13876
   343
             Sign.string_of_term sg t1);
chaieb@14920
   344
           ((pth RS iffD2) RS pre_thm,
berghofe@13876
   345
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
chaieb@14920
   346
    end
berghofe@13876
   347
      | _ => (pre_thm, assm_tac i)
chaieb@14758
   348
  in (rtac (((mp_step nh) o (spec_step np)) th) i 
chaieb@14758
   349
      THEN tac) st
berghofe@14130
   350
  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
berghofe@13876
   351
berghofe@13876
   352
fun presburger_args meth =
chaieb@14758
   353
 let val parse_flag = 
chaieb@14758
   354
         Args.$$$ "no_quantify" >> K (apfst (K false))
chaieb@18155
   355
      || Args.$$$ "no_abs" >> K (apsnd (K false));
chaieb@14758
   356
 in
chaieb@14758
   357
   Method.simple_args 
wenzelm@14882
   358
  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
chaieb@18155
   359
    curry (Library.foldl op |>) (true, true))
chaieb@14758
   360
    (fn (q,a) => fn _ => meth q a 1)
chaieb@14758
   361
  end;
berghofe@13876
   362
chaieb@14758
   363
fun presburger_method q a i = Method.METHOD (fn facts =>
chaieb@14758
   364
  Method.insert_tac facts 1 THEN presburger_tac q a i)
berghofe@13876
   365
berghofe@13876
   366
val setup =
wenzelm@18708
   367
  Method.add_method ("presburger",
wenzelm@18708
   368
    presburger_args presburger_method,
wenzelm@18708
   369
    "decision procedure for Presburger arithmetic") #>
wenzelm@18708
   370
  ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
wenzelm@18708
   371
    {splits = splits, inj_consts = inj_consts, discrete = discrete,
wenzelm@18708
   372
      presburger = SOME (presburger_tac true true)});
berghofe@13876
   373
berghofe@13876
   374
end;
berghofe@13876
   375
chaieb@18155
   376
val presburger_tac = Presburger.presburger_tac true true;