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