src/HOL/Integ/presburger.ML
author berghofe
Tue Mar 25 09:47:05 2003 +0100 (2003-03-25)
changeset 13876 68f4ed8311ac
child 13892 4ac9d55573da
permissions -rw-r--r--
New decision procedure for Presburger arithmetic.
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
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@13876
     5
berghofe@13876
     6
Tactic for solving arithmetical Goals in Presburger Arithmetic
berghofe@13876
     7
*)
berghofe@13876
     8
berghofe@13876
     9
signature PRESBURGER = 
berghofe@13876
    10
sig
berghofe@13876
    11
 val presburger_tac : bool -> int -> tactic
berghofe@13876
    12
 val presburger_method : bool -> int -> Proof.method
berghofe@13876
    13
 val setup : (theory -> theory) list
berghofe@13876
    14
 val trace : bool ref
berghofe@13876
    15
end;
berghofe@13876
    16
berghofe@13876
    17
structure Presburger: PRESBURGER =
berghofe@13876
    18
struct
berghofe@13876
    19
berghofe@13876
    20
val trace = ref false;
berghofe@13876
    21
fun trace_msg s = if !trace then tracing s else ();
berghofe@13876
    22
berghofe@13876
    23
(*-----------------------------------------------------------------*)
berghofe@13876
    24
(*cooper_pp: provefunction for the one-exstance quantifier elimination*)
berghofe@13876
    25
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
berghofe@13876
    26
(*-----------------------------------------------------------------*)
berghofe@13876
    27
berghofe@13876
    28
val presburger_ss = simpset_of (theory "Presburger");
berghofe@13876
    29
berghofe@13876
    30
fun cooper_pp sg vrl (fm as e$Abs(xn,xT,p)) = 
berghofe@13876
    31
  let val (xn1,p1) = variant_abs (xn,xT,p)
berghofe@13876
    32
  in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1 vrl) end;
berghofe@13876
    33
berghofe@13876
    34
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
berghofe@13876
    35
  (CooperProof.proof_of_evalc sg);
berghofe@13876
    36
berghofe@13876
    37
fun mproof_of_int_qelim sg fm =
berghofe@13876
    38
  Qelim.proof_of_mlift_qelim sg CooperDec.is_arith_rel
berghofe@13876
    39
    (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
berghofe@13876
    40
berghofe@13876
    41
(* Theorems to be used in this tactic*)
berghofe@13876
    42
berghofe@13876
    43
val zdvd_int = thm "zdvd_int";
berghofe@13876
    44
val zdiff_int_split = thm "zdiff_int_split";
berghofe@13876
    45
val all_nat = thm "all_nat";
berghofe@13876
    46
val ex_nat = thm "ex_nat";
berghofe@13876
    47
val number_of1 = thm "number_of1";
berghofe@13876
    48
val number_of2 = thm "number_of2";
berghofe@13876
    49
val split_zdiv = thm "split_zdiv";
berghofe@13876
    50
val split_zmod = thm "split_zmod";
berghofe@13876
    51
val mod_div_equality' = thm "mod_div_equality'";
berghofe@13876
    52
val split_div' = thm "split_div'";
berghofe@13876
    53
val Suc_plus1 = thm "Suc_plus1";
berghofe@13876
    54
val imp_le_cong = thm "imp_le_cong";
berghofe@13876
    55
val conj_le_cong = thm "conj_le_cong";
berghofe@13876
    56
berghofe@13876
    57
(* extract all the constants in a term*)
berghofe@13876
    58
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
berghofe@13876
    59
  | add_term_typed_consts (t $ u, cs) =
berghofe@13876
    60
      add_term_typed_consts (t, add_term_typed_consts (u, cs))
berghofe@13876
    61
  | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
berghofe@13876
    62
  | add_term_typed_consts (_, cs) = cs;
berghofe@13876
    63
berghofe@13876
    64
fun term_typed_consts t = add_term_typed_consts(t,[]);
berghofe@13876
    65
berghofe@13876
    66
(* put a term into eta long beta normal form *)
berghofe@13876
    67
fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
berghofe@13876
    68
  | eta_long Ts t = (case strip_comb t of
berghofe@13876
    69
      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
berghofe@13876
    70
    | (u, ts) => 
berghofe@13876
    71
      let val Us = binder_types (fastype_of1 (Ts, t))
berghofe@13876
    72
      in list_abs (map (pair "x") Us, Unify.combound
berghofe@13876
    73
        (list_comb (u, map (eta_long Ts) ts), 0, length Us))
berghofe@13876
    74
      end);
berghofe@13876
    75
berghofe@13876
    76
(* Some Types*)
berghofe@13876
    77
val bT = HOLogic.boolT;
berghofe@13876
    78
val iT = HOLogic.intT;
berghofe@13876
    79
val binT = HOLogic.binT;
berghofe@13876
    80
val nT = HOLogic.natT;
berghofe@13876
    81
berghofe@13876
    82
(* Allowed Consts in formulae for presburger tactic*)
berghofe@13876
    83
berghofe@13876
    84
val allowed_consts =
berghofe@13876
    85
  [("All", (iT --> bT) --> bT),
berghofe@13876
    86
   ("Ex", (iT --> bT) --> bT),
berghofe@13876
    87
   ("All", (nT --> bT) --> bT),
berghofe@13876
    88
   ("Ex", (nT --> bT) --> bT),
berghofe@13876
    89
berghofe@13876
    90
   ("op &", bT --> bT --> bT),
berghofe@13876
    91
   ("op |", bT --> bT --> bT),
berghofe@13876
    92
   ("op -->", bT --> bT --> bT),
berghofe@13876
    93
   ("op =", bT --> bT --> bT),
berghofe@13876
    94
   ("Not", bT --> bT),
berghofe@13876
    95
berghofe@13876
    96
   ("op <=", iT --> iT --> bT),
berghofe@13876
    97
   ("op =", iT --> iT --> bT),
berghofe@13876
    98
   ("op <", iT --> iT --> bT),
berghofe@13876
    99
   ("Divides.op dvd", iT --> iT --> bT),
berghofe@13876
   100
   ("Divides.op div", iT --> iT --> iT),
berghofe@13876
   101
   ("Divides.op mod", iT --> iT --> iT),
berghofe@13876
   102
   ("op +", iT --> iT --> iT),
berghofe@13876
   103
   ("op -", iT --> iT --> iT),
berghofe@13876
   104
   ("op *", iT --> iT --> iT), 
berghofe@13876
   105
   ("HOL.abs", iT --> iT),
berghofe@13876
   106
   ("uminus", iT --> iT),
berghofe@13876
   107
berghofe@13876
   108
   ("op <=", nT --> nT --> bT),
berghofe@13876
   109
   ("op =", nT --> nT --> bT),
berghofe@13876
   110
   ("op <", nT --> nT --> bT),
berghofe@13876
   111
   ("Divides.op dvd", nT --> nT --> bT),
berghofe@13876
   112
   ("Divides.op div", nT --> nT --> nT),
berghofe@13876
   113
   ("Divides.op mod", nT --> nT --> nT),
berghofe@13876
   114
   ("op +", nT --> nT --> nT),
berghofe@13876
   115
   ("op -", nT --> nT --> nT),
berghofe@13876
   116
   ("op *", nT --> nT --> nT), 
berghofe@13876
   117
   ("Suc", nT --> nT),
berghofe@13876
   118
berghofe@13876
   119
   ("Numeral.bin.Bit", binT --> bT --> binT),
berghofe@13876
   120
   ("Numeral.bin.Pls", binT),
berghofe@13876
   121
   ("Numeral.bin.Min", binT),
berghofe@13876
   122
   ("Numeral.number_of", binT --> iT),
berghofe@13876
   123
   ("Numeral.number_of", binT --> nT),
berghofe@13876
   124
   ("0", nT),
berghofe@13876
   125
   ("0", iT),
berghofe@13876
   126
   ("1", nT),
berghofe@13876
   127
   ("1", iT),
berghofe@13876
   128
berghofe@13876
   129
   ("False", bT),
berghofe@13876
   130
   ("True", bT)];
berghofe@13876
   131
berghofe@13876
   132
(*returns true if the formula is relevant for presburger arithmetic tactic*)
berghofe@13876
   133
fun relevant t = (term_typed_consts t) subset allowed_consts;
berghofe@13876
   134
berghofe@13876
   135
(* Preparation of the formula to be sent to the Integer quantifier *)
berghofe@13876
   136
(* elimination procedure                                           *)
berghofe@13876
   137
(* Transforms meta implications and meta quantifiers to object     *)
berghofe@13876
   138
(* implications and object quantifiers                             *)
berghofe@13876
   139
berghofe@13876
   140
fun prepare_for_presburger q fm = 
berghofe@13876
   141
  let
berghofe@13876
   142
    val ps = Logic.strip_params fm
berghofe@13876
   143
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
berghofe@13876
   144
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
berghofe@13876
   145
    val _ = if relevant c then () else raise CooperDec.COOPER
berghofe@13876
   146
    fun mk_all ((s, T), (P,n)) =
berghofe@13876
   147
      if 0 mem loose_bnos P then
berghofe@13876
   148
        (HOLogic.all_const T $ Abs (s, T, P), n)
berghofe@13876
   149
      else (incr_boundvars ~1 P, n-1)
berghofe@13876
   150
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
berghofe@13876
   151
    val (rhs,irhs) = partition relevant hs
berghofe@13876
   152
    val np = length ps
berghofe@13876
   153
    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
berghofe@13876
   154
      (ps,(foldr HOLogic.mk_imp (rhs, c), np))
berghofe@13876
   155
    val (vs, _) = partition (fn t => q orelse (type_of t) = nT)
berghofe@13876
   156
      (term_frees fm' @ term_vars fm');
berghofe@13876
   157
    val fm2 = foldr mk_all2 (vs, fm')
berghofe@13876
   158
  in (fm2, np + length vs, length rhs) end;
berghofe@13876
   159
berghofe@13876
   160
(*Object quantifier to meta --*)
berghofe@13876
   161
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
berghofe@13876
   162
berghofe@13876
   163
(* object implication to meta---*)
berghofe@13876
   164
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
berghofe@13876
   165
berghofe@13876
   166
(* the presburger tactic*)
berghofe@13876
   167
fun presburger_tac q i st =
berghofe@13876
   168
  let
berghofe@13876
   169
    val g = BasisLibrary.List.nth (prems_of st, i - 1);
berghofe@13876
   170
    val sg = sign_of_thm st;
berghofe@13876
   171
    (* Transform the term*)
berghofe@13876
   172
    val (t,np,nh) = prepare_for_presburger q g
berghofe@13876
   173
    (* Some simpsets for dealing with mod div abs and nat*)
berghofe@13876
   174
berghofe@13876
   175
    val simpset0 = HOL_basic_ss
berghofe@13876
   176
      addsimps [mod_div_equality', Suc_plus1]
berghofe@13876
   177
      addsplits [split_zdiv, split_zmod, split_div']
berghofe@13876
   178
    (* Simp rules for changing (n::int) to int n *)
berghofe@13876
   179
    val simpset1 = HOL_basic_ss
berghofe@13876
   180
      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
berghofe@13876
   181
        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
berghofe@13876
   182
      addsplits [zdiff_int_split]
berghofe@13876
   183
    (*simp rules for elimination of int n*)
berghofe@13876
   184
berghofe@13876
   185
    val simpset2 = HOL_basic_ss
berghofe@13876
   186
      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
berghofe@13876
   187
      addcongs [conj_le_cong, imp_le_cong]
berghofe@13876
   188
    (* simp rules for elimination of abs *)
berghofe@13876
   189
berghofe@13876
   190
    val simpset3 = HOL_basic_ss addsplits [zabs_split]
berghofe@13876
   191
	      
berghofe@13876
   192
    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
berghofe@13876
   193
berghofe@13876
   194
    (* Theorem for the nat --> int transformation *)
berghofe@13876
   195
    val pre_thm = Seq.hd (EVERY
berghofe@13876
   196
      [simp_tac simpset0 i,
berghofe@13876
   197
       TRY (simp_tac simpset1 i), TRY (simp_tac simpset2 i),
berghofe@13876
   198
       TRY (simp_tac simpset3 i), TRY (simp_tac presburger_ss i)]
berghofe@13876
   199
      (trivial ct))
berghofe@13876
   200
berghofe@13876
   201
    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i);
berghofe@13876
   202
berghofe@13876
   203
    (* The result of the quantifier elimination *)
berghofe@13876
   204
    val (th, tac) = case (prop_of pre_thm) of
berghofe@13876
   205
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
berghofe@13876
   206
          (trace_msg ("calling procedure with term:\n" ^
berghofe@13876
   207
             Sign.string_of_term sg t1);
berghofe@13876
   208
           ((mproof_of_int_qelim sg (eta_long [] t1) RS iffD2) RS pre_thm,
berghofe@13876
   209
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
berghofe@13876
   210
      | _ => (pre_thm, assm_tac i)
berghofe@13876
   211
  in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
berghofe@13876
   212
  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st;
berghofe@13876
   213
berghofe@13876
   214
fun presburger_args meth =
berghofe@13876
   215
  Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)
berghofe@13876
   216
    (fn q => fn _ => meth q 1);
berghofe@13876
   217
berghofe@13876
   218
fun presburger_method q i = Method.METHOD (fn facts =>
berghofe@13876
   219
  Method.insert_tac facts 1 THEN presburger_tac q i)
berghofe@13876
   220
berghofe@13876
   221
val setup =
berghofe@13876
   222
  [Method.add_method ("presburger",
berghofe@13876
   223
     presburger_args presburger_method,
berghofe@13876
   224
     "decision procedure for Presburger arithmetic"),
berghofe@13876
   225
   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
berghofe@13876
   226
     {splits = splits, inj_consts = inj_consts, discrete = discrete,
berghofe@13876
   227
      presburger = Some (presburger_tac true)})];
berghofe@13876
   228
berghofe@13876
   229
end;
berghofe@13876
   230
berghofe@13876
   231
val presburger_tac = Presburger.presburger_tac true;