src/HOL/Integ/presburger.ML
author chaieb
Fri Nov 11 10:49:59 2005 +0100 (2005-11-11)
changeset 18155 e5ab63ca6b0f
parent 17465 93fc1211603f
child 18202 46af82efd311
permissions -rw-r--r--
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
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
berghofe@13876
    17
 val setup : (theory -> theory) list
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");
berghofe@14801
    34
chaieb@14758
    35
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
berghofe@13876
    36
  let val (xn1,p1) = variant_abs (xn,xT,p)
chaieb@14758
    37
  in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
berghofe@13876
    38
berghofe@13876
    39
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
berghofe@13876
    40
  (CooperProof.proof_of_evalc sg);
berghofe@13876
    41
chaieb@14758
    42
fun tmproof_of_int_qelim sg fm =
chaieb@14758
    43
  Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
berghofe@13876
    44
    (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
berghofe@13876
    45
chaieb@14758
    46
berghofe@13876
    47
(* Theorems to be used in this tactic*)
berghofe@13876
    48
berghofe@13876
    49
val zdvd_int = thm "zdvd_int";
berghofe@13876
    50
val zdiff_int_split = thm "zdiff_int_split";
berghofe@13876
    51
val all_nat = thm "all_nat";
berghofe@13876
    52
val ex_nat = thm "ex_nat";
berghofe@13876
    53
val number_of1 = thm "number_of1";
berghofe@13876
    54
val number_of2 = thm "number_of2";
berghofe@13876
    55
val split_zdiv = thm "split_zdiv";
berghofe@13876
    56
val split_zmod = thm "split_zmod";
berghofe@13876
    57
val mod_div_equality' = thm "mod_div_equality'";
berghofe@13876
    58
val split_div' = thm "split_div'";
berghofe@13876
    59
val Suc_plus1 = thm "Suc_plus1";
berghofe@13876
    60
val imp_le_cong = thm "imp_le_cong";
berghofe@13876
    61
val conj_le_cong = thm "conj_le_cong";
berghofe@13876
    62
berghofe@13876
    63
(* extract all the constants in a term*)
berghofe@13876
    64
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
berghofe@13876
    65
  | add_term_typed_consts (t $ u, cs) =
berghofe@13876
    66
      add_term_typed_consts (t, add_term_typed_consts (u, cs))
berghofe@13876
    67
  | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
berghofe@13876
    68
  | add_term_typed_consts (_, cs) = cs;
berghofe@13876
    69
berghofe@13876
    70
fun term_typed_consts t = add_term_typed_consts(t,[]);
berghofe@13876
    71
wenzelm@15661
    72
(* Some Types*)
berghofe@13876
    73
val bT = HOLogic.boolT;
paulson@15620
    74
val bitT = HOLogic.bitT;
berghofe@13876
    75
val iT = HOLogic.intT;
berghofe@13876
    76
val binT = HOLogic.binT;
berghofe@13876
    77
val nT = HOLogic.natT;
berghofe@13876
    78
berghofe@13876
    79
(* Allowed Consts in formulae for presburger tactic*)
berghofe@13876
    80
berghofe@13876
    81
val allowed_consts =
berghofe@13876
    82
  [("All", (iT --> bT) --> bT),
berghofe@13876
    83
   ("Ex", (iT --> bT) --> bT),
berghofe@13876
    84
   ("All", (nT --> bT) --> bT),
berghofe@13876
    85
   ("Ex", (nT --> bT) --> bT),
berghofe@13876
    86
berghofe@13876
    87
   ("op &", bT --> bT --> bT),
berghofe@13876
    88
   ("op |", bT --> bT --> bT),
berghofe@13876
    89
   ("op -->", bT --> bT --> bT),
berghofe@13876
    90
   ("op =", bT --> bT --> bT),
berghofe@13876
    91
   ("Not", bT --> bT),
berghofe@13876
    92
berghofe@13876
    93
   ("op <=", iT --> iT --> bT),
berghofe@13876
    94
   ("op =", iT --> iT --> bT),
berghofe@13876
    95
   ("op <", iT --> iT --> bT),
berghofe@13876
    96
   ("Divides.op dvd", iT --> iT --> bT),
berghofe@13876
    97
   ("Divides.op div", iT --> iT --> iT),
berghofe@13876
    98
   ("Divides.op mod", iT --> iT --> iT),
berghofe@13876
    99
   ("op +", iT --> iT --> iT),
berghofe@13876
   100
   ("op -", iT --> iT --> iT),
berghofe@13876
   101
   ("op *", iT --> iT --> iT), 
berghofe@13876
   102
   ("HOL.abs", iT --> iT),
berghofe@13876
   103
   ("uminus", iT --> iT),
berghofe@14801
   104
   ("HOL.max", iT --> iT --> iT),
berghofe@14801
   105
   ("HOL.min", iT --> iT --> iT),
berghofe@13876
   106
berghofe@13876
   107
   ("op <=", nT --> nT --> bT),
berghofe@13876
   108
   ("op =", nT --> nT --> bT),
berghofe@13876
   109
   ("op <", nT --> nT --> bT),
berghofe@13876
   110
   ("Divides.op dvd", nT --> nT --> bT),
berghofe@13876
   111
   ("Divides.op div", nT --> nT --> nT),
berghofe@13876
   112
   ("Divides.op mod", nT --> nT --> nT),
berghofe@13876
   113
   ("op +", nT --> nT --> nT),
berghofe@13876
   114
   ("op -", nT --> nT --> nT),
berghofe@13876
   115
   ("op *", nT --> nT --> nT), 
berghofe@13876
   116
   ("Suc", nT --> nT),
berghofe@14801
   117
   ("HOL.max", nT --> nT --> nT),
berghofe@14801
   118
   ("HOL.min", nT --> nT --> nT),
berghofe@13876
   119
paulson@15620
   120
   ("Numeral.bit.B0", bitT),
paulson@15620
   121
   ("Numeral.bit.B1", bitT),
paulson@15620
   122
   ("Numeral.Bit", binT --> bitT --> binT),
paulson@15013
   123
   ("Numeral.Pls", binT),
paulson@15013
   124
   ("Numeral.Min", binT),
berghofe@13876
   125
   ("Numeral.number_of", binT --> iT),
berghofe@13876
   126
   ("Numeral.number_of", binT --> nT),
berghofe@13876
   127
   ("0", nT),
berghofe@13876
   128
   ("0", iT),
berghofe@13876
   129
   ("1", nT),
berghofe@13876
   130
   ("1", iT),
berghofe@13876
   131
   ("False", bT),
berghofe@13876
   132
   ("True", bT)];
berghofe@13876
   133
berghofe@13876
   134
(* Preparation of the formula to be sent to the Integer quantifier *)
berghofe@13876
   135
(* elimination procedure                                           *)
berghofe@13876
   136
(* Transforms meta implications and meta quantifiers to object     *)
berghofe@13876
   137
(* implications and object quantifiers                             *)
berghofe@13876
   138
chaieb@14758
   139
chaieb@14758
   140
(*==================================*)
chaieb@14758
   141
(* Abstracting on subterms  ========*)
chaieb@14758
   142
(*==================================*)
chaieb@14758
   143
(* Returns occurences of terms that are function application of type int or nat*)
chaieb@14758
   144
chaieb@14758
   145
fun getfuncs fm = case strip_comb fm of
chaieb@14758
   146
    (Free (_, T), ts as _ :: _) =>
chaieb@14758
   147
      if body_type T mem [iT, nT] 
chaieb@14758
   148
         andalso not (ts = []) andalso forall (null o loose_bnos) ts 
chaieb@14758
   149
      then [fm]
skalberg@15570
   150
      else Library.foldl op union ([], map getfuncs ts)
chaieb@14758
   151
  | (Var (_, T), ts as _ :: _) =>
chaieb@14758
   152
      if body_type T mem [iT, nT] 
chaieb@14758
   153
         andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
skalberg@15570
   154
      else Library.foldl op union ([], map getfuncs ts)
chaieb@14758
   155
  | (Const (s, T), ts) =>
chaieb@14758
   156
      if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
skalberg@15570
   157
      then Library.foldl op union ([], map getfuncs ts)
chaieb@14758
   158
      else [fm]
chaieb@14758
   159
  | (Abs (s, T, t), _) => getfuncs t
chaieb@14758
   160
  | _ => [];
chaieb@14758
   161
chaieb@14758
   162
chaieb@14758
   163
fun abstract_pres sg fm = 
skalberg@15574
   164
  foldr (fn (t, u) =>
chaieb@14758
   165
      let val T = fastype_of t
chaieb@14758
   166
      in all T $ Abs ("x", T, abstract_over (t, u)) end)
skalberg@15574
   167
         fm (getfuncs fm);
chaieb@14758
   168
chaieb@14758
   169
chaieb@14758
   170
chaieb@14758
   171
(* hasfuncs_on_bounds dont care of the type of the functions applied!
chaieb@14758
   172
 It returns true if there is a subterm coresponding to the application of
chaieb@14758
   173
 a function on a bounded variable.
chaieb@14758
   174
chaieb@14758
   175
 Function applications are allowed only for well predefined functions a 
chaieb@14758
   176
 consts*)
chaieb@14758
   177
chaieb@14758
   178
fun has_free_funcs fm  = case strip_comb fm of
chaieb@14758
   179
    (Free (_, T), ts as _ :: _) => 
chaieb@14758
   180
      if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
chaieb@14758
   181
      then true
chaieb@14758
   182
      else exists (fn x => x) (map has_free_funcs ts)
chaieb@14758
   183
  | (Var (_, T), ts as _ :: _) =>
chaieb@14758
   184
      if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
chaieb@14758
   185
      then true
chaieb@14758
   186
      else exists (fn x => x) (map has_free_funcs ts)
chaieb@14758
   187
  | (Const (s, T), ts) =>  exists (fn x => x) (map has_free_funcs ts)
chaieb@14758
   188
  | (Abs (s, T, t), _) => has_free_funcs t
chaieb@14758
   189
  |_ => false;
chaieb@14758
   190
chaieb@14758
   191
chaieb@14758
   192
(*returns true if the formula is relevant for presburger arithmetic tactic
chaieb@14758
   193
The constants occuring in term t should be a subset of the allowed_consts
chaieb@14758
   194
 There also should be no occurences of application of functions on bounded 
chaieb@14758
   195
 variables. Whenever this function will be used, it will be ensured that t 
chaieb@14758
   196
 will not contain subterms with function symbols that could have been 
chaieb@14758
   197
 abstracted over.*)
chaieb@14758
   198
 
chaieb@14758
   199
fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
skalberg@15570
   200
  map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
chaieb@14758
   201
  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
chaieb@14758
   202
  subset [iT, nT]
chaieb@14758
   203
  andalso not (has_free_funcs t);
chaieb@14758
   204
chaieb@14758
   205
chaieb@14758
   206
fun prepare_for_presburger sg q fm = 
berghofe@13876
   207
  let
berghofe@13876
   208
    val ps = Logic.strip_params fm
berghofe@13876
   209
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
berghofe@13876
   210
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
chaieb@14758
   211
    val _ = if relevant (rev ps) c then () 
chaieb@14758
   212
               else  (trace_msg ("Conclusion is not a presburger term:\n" ^
chaieb@14758
   213
             Sign.string_of_term sg c); raise CooperDec.COOPER)
berghofe@13876
   214
    fun mk_all ((s, T), (P,n)) =
berghofe@13876
   215
      if 0 mem loose_bnos P then
berghofe@13876
   216
        (HOLogic.all_const T $ Abs (s, T, P), n)
berghofe@13876
   217
      else (incr_boundvars ~1 P, n-1)
berghofe@13876
   218
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
skalberg@15570
   219
    val (rhs,irhs) = List.partition (relevant (rev ps)) hs
berghofe@13876
   220
    val np = length ps
skalberg@15574
   221
    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
skalberg@15574
   222
      (foldr HOLogic.mk_imp c rhs, np) ps
skalberg@15570
   223
    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
berghofe@13876
   224
      (term_frees fm' @ term_vars fm');
skalberg@15574
   225
    val fm2 = foldr mk_all2 fm' vs
berghofe@13876
   226
  in (fm2, np + length vs, length rhs) end;
berghofe@13876
   227
berghofe@13876
   228
(*Object quantifier to meta --*)
berghofe@13876
   229
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
berghofe@13876
   230
berghofe@13876
   231
(* object implication to meta---*)
berghofe@13876
   232
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
berghofe@13876
   233
berghofe@13876
   234
(* the presburger tactic*)
chaieb@14758
   235
chaieb@14758
   236
(* Parameters : q = flag for quantify ofer free variables ; 
chaieb@14758
   237
                a = flag for abstracting over function occurences
chaieb@14758
   238
                i = subgoal  *)
chaieb@14758
   239
chaieb@14758
   240
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
berghofe@13876
   241
  let
wenzelm@17465
   242
    val g = List.nth (prems_of st, i - 1)
chaieb@14758
   243
    val sg = sign_of_thm st
chaieb@14758
   244
    (* The Abstraction step *)
chaieb@14758
   245
    val g' = if a then abstract_pres sg g else g
berghofe@13876
   246
    (* Transform the term*)
chaieb@14758
   247
    val (t,np,nh) = prepare_for_presburger sg q g'
wenzelm@15661
   248
    (* Some simpsets for dealing with mod div abs and nat*)
berghofe@13876
   249
    val simpset0 = HOL_basic_ss
berghofe@13876
   250
      addsimps [mod_div_equality', Suc_plus1]
berghofe@13997
   251
      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
berghofe@13876
   252
    (* Simp rules for changing (n::int) to int n *)
berghofe@13876
   253
    val simpset1 = HOL_basic_ss
berghofe@13876
   254
      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
berghofe@13876
   255
        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
berghofe@13876
   256
      addsplits [zdiff_int_split]
berghofe@13876
   257
    (*simp rules for elimination of int n*)
berghofe@13876
   258
berghofe@13876
   259
    val simpset2 = HOL_basic_ss
berghofe@13876
   260
      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
berghofe@13876
   261
      addcongs [conj_le_cong, imp_le_cong]
berghofe@13876
   262
    (* simp rules for elimination of abs *)
paulson@14353
   263
    val simpset3 = HOL_basic_ss addsplits [abs_split]
berghofe@13876
   264
    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
berghofe@13876
   265
    (* Theorem for the nat --> int transformation *)
berghofe@13876
   266
    val pre_thm = Seq.hd (EVERY
chaieb@14758
   267
      [simp_tac simpset0 1,
chaieb@14758
   268
       TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
berghofe@14801
   269
       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
berghofe@13876
   270
      (trivial ct))
chaieb@14758
   271
    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
berghofe@13876
   272
    (* The result of the quantifier elimination *)
berghofe@13876
   273
    val (th, tac) = case (prop_of pre_thm) of
berghofe@13876
   274
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
chaieb@14920
   275
    let val pth = 
chaieb@14920
   276
          (* If quick_and_dirty then run without proof generation as oracle*)
chaieb@14920
   277
             if !quick_and_dirty 
wenzelm@16836
   278
             then presburger_oracle sg (Pattern.eta_long [] t1)
chaieb@14941
   279
(*
chaieb@14941
   280
assume (cterm_of sg 
chaieb@14920
   281
	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
chaieb@14941
   282
*)
chaieb@14920
   283
	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
chaieb@14920
   284
    in 
berghofe@13876
   285
          (trace_msg ("calling procedure with term:\n" ^
berghofe@13876
   286
             Sign.string_of_term sg t1);
chaieb@14920
   287
           ((pth RS iffD2) RS pre_thm,
berghofe@13876
   288
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
chaieb@14920
   289
    end
berghofe@13876
   290
      | _ => (pre_thm, assm_tac i)
chaieb@14758
   291
  in (rtac (((mp_step nh) o (spec_step np)) th) i 
chaieb@14758
   292
      THEN tac) st
berghofe@14130
   293
  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
berghofe@13876
   294
berghofe@13876
   295
fun presburger_args meth =
chaieb@14758
   296
 let val parse_flag = 
chaieb@14758
   297
         Args.$$$ "no_quantify" >> K (apfst (K false))
chaieb@18155
   298
      || Args.$$$ "no_abs" >> K (apsnd (K false));
chaieb@14758
   299
 in
chaieb@14758
   300
   Method.simple_args 
wenzelm@14882
   301
  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
chaieb@18155
   302
    curry (Library.foldl op |>) (true, true))
chaieb@14758
   303
    (fn (q,a) => fn _ => meth q a 1)
chaieb@14758
   304
  end;
berghofe@13876
   305
chaieb@14758
   306
fun presburger_method q a i = Method.METHOD (fn facts =>
chaieb@14758
   307
  Method.insert_tac facts 1 THEN presburger_tac q a i)
berghofe@13876
   308
berghofe@13876
   309
val setup =
berghofe@13876
   310
  [Method.add_method ("presburger",
berghofe@13876
   311
     presburger_args presburger_method,
berghofe@13876
   312
     "decision procedure for Presburger arithmetic"),
berghofe@13876
   313
   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
berghofe@13876
   314
     {splits = splits, inj_consts = inj_consts, discrete = discrete,
chaieb@18155
   315
      presburger = SOME (presburger_tac true true)})];
berghofe@13876
   316
berghofe@13876
   317
end;
berghofe@13876
   318
chaieb@18155
   319
val presburger_tac = Presburger.presburger_tac true true;