src/HOL/Integ/presburger.ML
author berghofe
Sat May 10 20:52:18 2003 +0200 (2003-05-10)
changeset 13997 3d53dcd77877
parent 13892 4ac9d55573da
child 14130 398bc4a885d6
permissions -rw-r--r--
- Added split_min and split_max to preprocessor
- Moved eta_long to Pure/pattern.ML
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
(* Some Types*)
berghofe@13876
    67
val bT = HOLogic.boolT;
berghofe@13876
    68
val iT = HOLogic.intT;
berghofe@13876
    69
val binT = HOLogic.binT;
berghofe@13876
    70
val nT = HOLogic.natT;
berghofe@13876
    71
berghofe@13876
    72
(* Allowed Consts in formulae for presburger tactic*)
berghofe@13876
    73
berghofe@13876
    74
val allowed_consts =
berghofe@13876
    75
  [("All", (iT --> bT) --> bT),
berghofe@13876
    76
   ("Ex", (iT --> bT) --> bT),
berghofe@13876
    77
   ("All", (nT --> bT) --> bT),
berghofe@13876
    78
   ("Ex", (nT --> bT) --> bT),
berghofe@13876
    79
berghofe@13876
    80
   ("op &", bT --> bT --> bT),
berghofe@13876
    81
   ("op |", bT --> bT --> bT),
berghofe@13876
    82
   ("op -->", bT --> bT --> bT),
berghofe@13876
    83
   ("op =", bT --> bT --> bT),
berghofe@13876
    84
   ("Not", bT --> bT),
berghofe@13876
    85
berghofe@13876
    86
   ("op <=", iT --> iT --> bT),
berghofe@13876
    87
   ("op =", iT --> iT --> bT),
berghofe@13876
    88
   ("op <", iT --> iT --> bT),
berghofe@13876
    89
   ("Divides.op dvd", iT --> iT --> bT),
berghofe@13876
    90
   ("Divides.op div", iT --> iT --> iT),
berghofe@13876
    91
   ("Divides.op mod", iT --> iT --> iT),
berghofe@13876
    92
   ("op +", iT --> iT --> iT),
berghofe@13876
    93
   ("op -", iT --> iT --> iT),
berghofe@13876
    94
   ("op *", iT --> iT --> iT), 
berghofe@13876
    95
   ("HOL.abs", iT --> iT),
berghofe@13876
    96
   ("uminus", iT --> iT),
berghofe@13997
    97
   ("HOL.max", iT --> iT --> iT),
berghofe@13997
    98
   ("HOL.min", iT --> iT --> iT),
berghofe@13876
    99
berghofe@13876
   100
   ("op <=", nT --> nT --> bT),
berghofe@13876
   101
   ("op =", nT --> nT --> bT),
berghofe@13876
   102
   ("op <", nT --> nT --> bT),
berghofe@13876
   103
   ("Divides.op dvd", nT --> nT --> bT),
berghofe@13876
   104
   ("Divides.op div", nT --> nT --> nT),
berghofe@13876
   105
   ("Divides.op mod", nT --> nT --> nT),
berghofe@13876
   106
   ("op +", nT --> nT --> nT),
berghofe@13876
   107
   ("op -", nT --> nT --> nT),
berghofe@13876
   108
   ("op *", nT --> nT --> nT), 
berghofe@13876
   109
   ("Suc", nT --> nT),
berghofe@13997
   110
   ("HOL.max", nT --> nT --> nT),
berghofe@13997
   111
   ("HOL.min", nT --> nT --> nT),
berghofe@13876
   112
berghofe@13876
   113
   ("Numeral.bin.Bit", binT --> bT --> binT),
berghofe@13876
   114
   ("Numeral.bin.Pls", binT),
berghofe@13876
   115
   ("Numeral.bin.Min", binT),
berghofe@13876
   116
   ("Numeral.number_of", binT --> iT),
berghofe@13876
   117
   ("Numeral.number_of", binT --> nT),
berghofe@13876
   118
   ("0", nT),
berghofe@13876
   119
   ("0", iT),
berghofe@13876
   120
   ("1", nT),
berghofe@13876
   121
   ("1", iT),
berghofe@13876
   122
berghofe@13876
   123
   ("False", bT),
berghofe@13876
   124
   ("True", bT)];
berghofe@13876
   125
berghofe@13876
   126
(*returns true if the formula is relevant for presburger arithmetic tactic*)
berghofe@13876
   127
fun relevant t = (term_typed_consts t) subset allowed_consts;
berghofe@13876
   128
berghofe@13876
   129
(* Preparation of the formula to be sent to the Integer quantifier *)
berghofe@13876
   130
(* elimination procedure                                           *)
berghofe@13876
   131
(* Transforms meta implications and meta quantifiers to object     *)
berghofe@13876
   132
(* implications and object quantifiers                             *)
berghofe@13876
   133
berghofe@13876
   134
fun prepare_for_presburger q fm = 
berghofe@13876
   135
  let
berghofe@13876
   136
    val ps = Logic.strip_params fm
berghofe@13876
   137
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
berghofe@13876
   138
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
berghofe@13876
   139
    val _ = if relevant c then () else raise CooperDec.COOPER
berghofe@13876
   140
    fun mk_all ((s, T), (P,n)) =
berghofe@13876
   141
      if 0 mem loose_bnos P then
berghofe@13876
   142
        (HOLogic.all_const T $ Abs (s, T, P), n)
berghofe@13876
   143
      else (incr_boundvars ~1 P, n-1)
berghofe@13876
   144
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
berghofe@13876
   145
    val (rhs,irhs) = partition relevant hs
berghofe@13876
   146
    val np = length ps
berghofe@13876
   147
    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
berghofe@13876
   148
      (ps,(foldr HOLogic.mk_imp (rhs, c), np))
berghofe@13876
   149
    val (vs, _) = partition (fn t => q orelse (type_of t) = nT)
berghofe@13876
   150
      (term_frees fm' @ term_vars fm');
berghofe@13876
   151
    val fm2 = foldr mk_all2 (vs, fm')
berghofe@13876
   152
  in (fm2, np + length vs, length rhs) end;
berghofe@13876
   153
berghofe@13876
   154
(*Object quantifier to meta --*)
berghofe@13876
   155
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
berghofe@13876
   156
berghofe@13876
   157
(* object implication to meta---*)
berghofe@13876
   158
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
berghofe@13876
   159
berghofe@13876
   160
(* the presburger tactic*)
berghofe@13876
   161
fun presburger_tac q i st =
berghofe@13876
   162
  let
berghofe@13876
   163
    val g = BasisLibrary.List.nth (prems_of st, i - 1);
berghofe@13876
   164
    val sg = sign_of_thm st;
berghofe@13876
   165
    (* Transform the term*)
berghofe@13876
   166
    val (t,np,nh) = prepare_for_presburger q g
berghofe@13876
   167
    (* Some simpsets for dealing with mod div abs and nat*)
berghofe@13876
   168
berghofe@13876
   169
    val simpset0 = HOL_basic_ss
berghofe@13876
   170
      addsimps [mod_div_equality', Suc_plus1]
berghofe@13997
   171
      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
berghofe@13876
   172
    (* Simp rules for changing (n::int) to int n *)
berghofe@13876
   173
    val simpset1 = HOL_basic_ss
berghofe@13876
   174
      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
berghofe@13876
   175
        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
berghofe@13876
   176
      addsplits [zdiff_int_split]
berghofe@13876
   177
    (*simp rules for elimination of int n*)
berghofe@13876
   178
berghofe@13876
   179
    val simpset2 = HOL_basic_ss
berghofe@13876
   180
      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
berghofe@13876
   181
      addcongs [conj_le_cong, imp_le_cong]
berghofe@13876
   182
    (* simp rules for elimination of abs *)
berghofe@13876
   183
berghofe@13876
   184
    val simpset3 = HOL_basic_ss addsplits [zabs_split]
berghofe@13876
   185
	      
berghofe@13876
   186
    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
berghofe@13876
   187
berghofe@13876
   188
    (* Theorem for the nat --> int transformation *)
berghofe@13876
   189
    val pre_thm = Seq.hd (EVERY
berghofe@13876
   190
      [simp_tac simpset0 i,
berghofe@13876
   191
       TRY (simp_tac simpset1 i), TRY (simp_tac simpset2 i),
berghofe@13876
   192
       TRY (simp_tac simpset3 i), TRY (simp_tac presburger_ss i)]
berghofe@13876
   193
      (trivial ct))
berghofe@13876
   194
berghofe@13876
   195
    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i);
berghofe@13876
   196
berghofe@13876
   197
    (* The result of the quantifier elimination *)
berghofe@13876
   198
    val (th, tac) = case (prop_of pre_thm) of
berghofe@13876
   199
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
berghofe@13876
   200
          (trace_msg ("calling procedure with term:\n" ^
berghofe@13876
   201
             Sign.string_of_term sg t1);
berghofe@13997
   202
           ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
berghofe@13876
   203
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
berghofe@13876
   204
      | _ => (pre_thm, assm_tac i)
berghofe@13876
   205
  in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
berghofe@13876
   206
  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st;
berghofe@13876
   207
berghofe@13876
   208
fun presburger_args meth =
berghofe@13876
   209
  Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)
berghofe@13876
   210
    (fn q => fn _ => meth q 1);
berghofe@13876
   211
berghofe@13876
   212
fun presburger_method q i = Method.METHOD (fn facts =>
berghofe@13876
   213
  Method.insert_tac facts 1 THEN presburger_tac q i)
berghofe@13876
   214
berghofe@13876
   215
val setup =
berghofe@13876
   216
  [Method.add_method ("presburger",
berghofe@13876
   217
     presburger_args presburger_method,
berghofe@13876
   218
     "decision procedure for Presburger arithmetic"),
berghofe@13876
   219
   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
berghofe@13876
   220
     {splits = splits, inj_consts = inj_consts, discrete = discrete,
berghofe@13876
   221
      presburger = Some (presburger_tac true)})];
berghofe@13876
   222
berghofe@13876
   223
end;
berghofe@13876
   224
berghofe@13876
   225
val presburger_tac = Presburger.presburger_tac true;