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