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