src/HOL/Tools/Presburger/presburger.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 18708 4b3dadb4fe33
child 19233 77ca20b0ed77
permissions -rw-r--r--
improved code generator devarification
     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 This version of presburger deals with occurences of functional symbols
     8 in the subgoal and abstract over them to try to prove the more general
     9 formula. It then resolves with the subgoal. To enable this feature
    10 call the procedure with the parameter abs.
    11 *)
    12 
    13 signature PRESBURGER = 
    14 sig
    15  val presburger_tac : bool -> bool -> int -> tactic
    16  val presburger_method : bool -> bool -> int -> Proof.method
    17  val setup : theory -> theory
    18  val trace : bool ref
    19 end;
    20 
    21 structure Presburger: PRESBURGER =
    22 struct
    23 
    24 val trace = ref false;
    25 fun trace_msg s = if !trace then tracing s else ();
    26 
    27 (*-----------------------------------------------------------------*)
    28 (*cooper_pp: provefunction for the one-exstance quantifier elimination*)
    29 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
    30 (*-----------------------------------------------------------------*)
    31 
    32 
    33 val presburger_ss = simpset_of (theory "Presburger");
    34 val binarith = map thm
    35   ["Pls_0_eq", "Min_1_eq",
    36  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    37   "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    38   "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
    39   "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
    40   "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
    41   "bin_add_Pls_right", "bin_add_Min_right"];
    42  val intarithrel = 
    43      (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
    44 		"int_le_number_of_eq","int_iszero_number_of_0",
    45 		"int_less_number_of_eq_neg"]) @
    46      (map (fn s => thm s RS thm "lift_bool") 
    47 	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    48 	   "int_neg_number_of_Min"])@
    49      (map (fn s => thm s RS thm "nlift_bool") 
    50 	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    51      
    52 val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    53 			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    54 val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    55 			"mult_nat_number_of", "eq_nat_number_of",
    56 			"less_nat_number_of"]
    57 val powerarith = 
    58     (map thm ["nat_number_of", "zpower_number_of_even", 
    59 	      "zpower_Pls", "zpower_Min"]) @ 
    60     [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
    61 			   thm "one_eq_Numeral1_nring"] 
    62   (thm "zpower_number_of_odd"))]
    63 
    64 val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    65 	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    66 
    67 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    68   let val (xn1,p1) = variant_abs (xn,xT,p)
    69   in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
    70 
    71 fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
    72   (CooperProof.proof_of_evalc sg);
    73 
    74 fun tmproof_of_int_qelim sg fm =
    75   Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
    76     (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
    77 
    78 
    79 (* Theorems to be used in this tactic*)
    80 
    81 val zdvd_int = thm "zdvd_int";
    82 val zdiff_int_split = thm "zdiff_int_split";
    83 val all_nat = thm "all_nat";
    84 val ex_nat = thm "ex_nat";
    85 val number_of1 = thm "number_of1";
    86 val number_of2 = thm "number_of2";
    87 val split_zdiv = thm "split_zdiv";
    88 val split_zmod = thm "split_zmod";
    89 val mod_div_equality' = thm "mod_div_equality'";
    90 val split_div' = thm "split_div'";
    91 val Suc_plus1 = thm "Suc_plus1";
    92 val imp_le_cong = thm "imp_le_cong";
    93 val conj_le_cong = thm "conj_le_cong";
    94 val nat_mod_add_eq = mod_add1_eq RS sym;
    95 val nat_mod_add_left_eq = mod_add_left_eq RS sym;
    96 val nat_mod_add_right_eq = mod_add_right_eq RS sym;
    97 val int_mod_add_eq = zmod_zadd1_eq RS sym;
    98 val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
    99 val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
   100 val nat_div_add_eq = div_add1_eq RS sym;
   101 val int_div_add_eq = zdiv_zadd1_eq RS sym;
   102 val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
   103 val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
   104 
   105 
   106 (* extract all the constants in a term*)
   107 fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
   108   | add_term_typed_consts (t $ u, cs) =
   109       add_term_typed_consts (t, add_term_typed_consts (u, cs))
   110   | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
   111   | add_term_typed_consts (_, cs) = cs;
   112 
   113 fun term_typed_consts t = add_term_typed_consts(t,[]);
   114 
   115 (* Some Types*)
   116 val bT = HOLogic.boolT;
   117 val bitT = HOLogic.bitT;
   118 val iT = HOLogic.intT;
   119 val binT = HOLogic.binT;
   120 val nT = HOLogic.natT;
   121 
   122 (* Allowed Consts in formulae for presburger tactic*)
   123 
   124 val allowed_consts =
   125   [("All", (iT --> bT) --> bT),
   126    ("Ex", (iT --> bT) --> bT),
   127    ("All", (nT --> bT) --> bT),
   128    ("Ex", (nT --> bT) --> bT),
   129 
   130    ("op &", bT --> bT --> bT),
   131    ("op |", bT --> bT --> bT),
   132    ("op -->", bT --> bT --> bT),
   133    ("op =", bT --> bT --> bT),
   134    ("Not", bT --> bT),
   135 
   136    ("op <=", iT --> iT --> bT),
   137    ("op =", iT --> iT --> bT),
   138    ("op <", iT --> iT --> bT),
   139    ("Divides.op dvd", iT --> iT --> bT),
   140    ("Divides.op div", iT --> iT --> iT),
   141    ("Divides.op mod", iT --> iT --> iT),
   142    ("op +", iT --> iT --> iT),
   143    ("op -", iT --> iT --> iT),
   144    ("op *", iT --> iT --> iT), 
   145    ("HOL.abs", iT --> iT),
   146    ("uminus", iT --> iT),
   147    ("HOL.max", iT --> iT --> iT),
   148    ("HOL.min", iT --> iT --> iT),
   149 
   150    ("op <=", nT --> nT --> bT),
   151    ("op =", nT --> nT --> bT),
   152    ("op <", nT --> nT --> bT),
   153    ("Divides.op dvd", nT --> nT --> bT),
   154    ("Divides.op div", nT --> nT --> nT),
   155    ("Divides.op mod", nT --> nT --> nT),
   156    ("op +", nT --> nT --> nT),
   157    ("op -", nT --> nT --> nT),
   158    ("op *", nT --> nT --> nT), 
   159    ("Suc", nT --> nT),
   160    ("HOL.max", nT --> nT --> nT),
   161    ("HOL.min", nT --> nT --> nT),
   162 
   163    ("Numeral.bit.B0", bitT),
   164    ("Numeral.bit.B1", bitT),
   165    ("Numeral.Bit", binT --> bitT --> binT),
   166    ("Numeral.Pls", binT),
   167    ("Numeral.Min", binT),
   168    ("Numeral.number_of", binT --> iT),
   169    ("Numeral.number_of", binT --> nT),
   170    ("0", nT),
   171    ("0", iT),
   172    ("1", nT),
   173    ("1", iT),
   174    ("False", bT),
   175    ("True", bT)];
   176 
   177 (* Preparation of the formula to be sent to the Integer quantifier *)
   178 (* elimination procedure                                           *)
   179 (* Transforms meta implications and meta quantifiers to object     *)
   180 (* implications and object quantifiers                             *)
   181 
   182 
   183 (*==================================*)
   184 (* Abstracting on subterms  ========*)
   185 (*==================================*)
   186 (* Returns occurences of terms that are function application of type int or nat*)
   187 
   188 fun getfuncs fm = case strip_comb fm of
   189     (Free (_, T), ts as _ :: _) =>
   190       if body_type T mem [iT, nT] 
   191          andalso not (ts = []) andalso forall (null o loose_bnos) ts 
   192       then [fm]
   193       else Library.foldl op union ([], map getfuncs ts)
   194   | (Var (_, T), ts as _ :: _) =>
   195       if body_type T mem [iT, nT] 
   196          andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
   197       else Library.foldl op union ([], map getfuncs ts)
   198   | (Const (s, T), ts) =>
   199       if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
   200       then Library.foldl op union ([], map getfuncs ts)
   201       else [fm]
   202   | (Abs (s, T, t), _) => getfuncs t
   203   | _ => [];
   204 
   205 
   206 fun abstract_pres sg fm = 
   207   foldr (fn (t, u) =>
   208       let val T = fastype_of t
   209       in all T $ Abs ("x", T, abstract_over (t, u)) end)
   210          fm (getfuncs fm);
   211 
   212 
   213 
   214 (* hasfuncs_on_bounds dont care of the type of the functions applied!
   215  It returns true if there is a subterm coresponding to the application of
   216  a function on a bounded variable.
   217 
   218  Function applications are allowed only for well predefined functions a 
   219  consts*)
   220 
   221 fun has_free_funcs fm  = case strip_comb fm of
   222     (Free (_, T), ts as _ :: _) => 
   223       if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
   224       then true
   225       else exists (fn x => x) (map has_free_funcs ts)
   226   | (Var (_, T), ts as _ :: _) =>
   227       if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
   228       then true
   229       else exists (fn x => x) (map has_free_funcs ts)
   230   | (Const (s, T), ts) =>  exists (fn x => x) (map has_free_funcs ts)
   231   | (Abs (s, T, t), _) => has_free_funcs t
   232   |_ => false;
   233 
   234 
   235 (*returns true if the formula is relevant for presburger arithmetic tactic
   236 The constants occuring in term t should be a subset of the allowed_consts
   237  There also should be no occurences of application of functions on bounded 
   238  variables. Whenever this function will be used, it will be ensured that t 
   239  will not contain subterms with function symbols that could have been 
   240  abstracted over.*)
   241  
   242 fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
   243   map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
   244   map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
   245   subset [iT, nT]
   246   andalso not (has_free_funcs t);
   247 
   248 
   249 fun prepare_for_presburger sg q fm = 
   250   let
   251     val ps = Logic.strip_params fm
   252     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
   253     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
   254     val _ = if relevant (rev ps) c then () 
   255                else  (trace_msg ("Conclusion is not a presburger term:\n" ^
   256              Sign.string_of_term sg c); raise CooperDec.COOPER)
   257     fun mk_all ((s, T), (P,n)) =
   258       if 0 mem loose_bnos P then
   259         (HOLogic.all_const T $ Abs (s, T, P), n)
   260       else (incr_boundvars ~1 P, n-1)
   261     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
   262     val (rhs,irhs) = List.partition (relevant (rev ps)) hs
   263     val np = length ps
   264     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   265       (foldr HOLogic.mk_imp c rhs, np) ps
   266     val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
   267       (term_frees fm' @ term_vars fm');
   268     val fm2 = foldr mk_all2 fm' vs
   269   in (fm2, np + length vs, length rhs) end;
   270 
   271 (*Object quantifier to meta --*)
   272 fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
   273 
   274 (* object implication to meta---*)
   275 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
   276 
   277 (* the presburger tactic*)
   278 
   279 (* Parameters : q = flag for quantify ofer free variables ; 
   280                 a = flag for abstracting over function occurences
   281                 i = subgoal  *)
   282 
   283 fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
   284   let
   285     val g = List.nth (prems_of st, i - 1)
   286     val sg = sign_of_thm st
   287     (* The Abstraction step *)
   288     val g' = if a then abstract_pres sg g else g
   289     (* Transform the term*)
   290     val (t,np,nh) = prepare_for_presburger sg q g'
   291     (* Some simpsets for dealing with mod div abs and nat*)
   292     val mod_div_simpset = HOL_basic_ss 
   293 			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
   294 				  nat_mod_add_right_eq, int_mod_add_eq, 
   295 				  int_mod_add_right_eq, int_mod_add_left_eq,
   296 				  nat_div_add_eq, int_div_add_eq,
   297 				  mod_self, zmod_self,
   298 				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
   299 				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
   300 				  zdiv_zero,zmod_zero,div_0,mod_0,
   301 				  zdiv_1,zmod_1,div_1,mod_1,
   302 				  Suc_plus1]
   303 			addsimps add_ac
   304 			addsimprocs [cancel_div_mod_proc]
   305     val simpset0 = HOL_basic_ss
   306       addsimps [mod_div_equality', Suc_plus1]
   307       addsimps comp_arith
   308       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
   309     (* Simp rules for changing (n::int) to int n *)
   310     val simpset1 = HOL_basic_ss
   311       addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
   312         [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
   313       addsplits [zdiff_int_split]
   314     (*simp rules for elimination of int n*)
   315 
   316     val simpset2 = HOL_basic_ss
   317       addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
   318       addcongs [conj_le_cong, imp_le_cong]
   319     (* simp rules for elimination of abs *)
   320     val simpset3 = HOL_basic_ss addsplits [abs_split]
   321     val ct = cterm_of sg (HOLogic.mk_Trueprop t)
   322     (* Theorem for the nat --> int transformation *)
   323     val pre_thm = Seq.hd (EVERY
   324       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
   325        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
   326        TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
   327       (trivial ct))
   328     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
   329     (* The result of the quantifier elimination *)
   330     val (th, tac) = case (prop_of pre_thm) of
   331         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
   332     let val pth = 
   333           (* If quick_and_dirty then run without proof generation as oracle*)
   334              if !quick_and_dirty 
   335              then presburger_oracle sg (Pattern.eta_long [] t1)
   336 (*
   337 assume (cterm_of sg 
   338 	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
   339 *)
   340 	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
   341     in 
   342           (trace_msg ("calling procedure with term:\n" ^
   343              Sign.string_of_term sg t1);
   344            ((pth RS iffD2) RS pre_thm,
   345             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
   346     end
   347       | _ => (pre_thm, assm_tac i)
   348   in (rtac (((mp_step nh) o (spec_step np)) th) i 
   349       THEN tac) st
   350   end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
   351 
   352 fun presburger_args meth =
   353  let val parse_flag = 
   354          Args.$$$ "no_quantify" >> K (apfst (K false))
   355       || Args.$$$ "no_abs" >> K (apsnd (K false));
   356  in
   357    Method.simple_args 
   358   (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   359     curry (Library.foldl op |>) (true, true))
   360     (fn (q,a) => fn _ => meth q a 1)
   361   end;
   362 
   363 fun presburger_method q a i = Method.METHOD (fn facts =>
   364   Method.insert_tac facts 1 THEN presburger_tac q a i)
   365 
   366 val setup =
   367   Method.add_method ("presburger",
   368     presburger_args presburger_method,
   369     "decision procedure for Presburger arithmetic") #>
   370   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
   371     {splits = splits, inj_consts = inj_consts, discrete = discrete,
   372       presburger = SOME (presburger_tac true true)});
   373 
   374 end;
   375 
   376 val presburger_tac = Presburger.presburger_tac true true;