src/HOL/Integ/presburger.ML

Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers

(*  Title:      HOL/Integ/presburger.ML
    ID:         $Id$
    Author:     Amine Chaieb and Stefan Berghofer, TU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Tactic for solving arithmetical Goals in Presburger Arithmetic
*)

signature PRESBURGER = 
sig
 val presburger_tac : bool -> int -> tactic
 val presburger_method : bool -> int -> Proof.method
 val setup : (theory -> theory) list
 val trace : bool ref
end;

structure Presburger: PRESBURGER =
struct

val trace = ref false;
fun trace_msg s = if !trace then tracing s else ();

(*-----------------------------------------------------------------*)
(*cooper_pp: provefunction for the one-exstance quantifier elimination*)
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
(*-----------------------------------------------------------------*)

val presburger_ss = simpset_of (theory "Presburger");

fun cooper_pp sg vrl (fm as e$Abs(xn,xT,p)) = 
  let val (xn1,p1) = variant_abs (xn,xT,p)
  in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1 vrl) end;

fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
  (CooperProof.proof_of_evalc sg);

fun mproof_of_int_qelim sg fm =
  Qelim.proof_of_mlift_qelim sg CooperDec.is_arith_rel
    (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;

(* Theorems to be used in this tactic*)

val zdvd_int = thm "zdvd_int";
val zdiff_int_split = thm "zdiff_int_split";
val all_nat = thm "all_nat";
val ex_nat = thm "ex_nat";
val number_of1 = thm "number_of1";
val number_of2 = thm "number_of2";
val split_zdiv = thm "split_zdiv";
val split_zmod = thm "split_zmod";
val mod_div_equality' = thm "mod_div_equality'";
val split_div' = thm "split_div'";
val Suc_plus1 = thm "Suc_plus1";
val imp_le_cong = thm "imp_le_cong";
val conj_le_cong = thm "conj_le_cong";

(* extract all the constants in a term*)
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
  | add_term_typed_consts (t $ u, cs) =
      add_term_typed_consts (t, add_term_typed_consts (u, cs))
  | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
  | add_term_typed_consts (_, cs) = cs;

fun term_typed_consts t = add_term_typed_consts(t,[]);

(* Some Types*)
val bT = HOLogic.boolT;
val iT = HOLogic.intT;
val binT = HOLogic.binT;
val nT = HOLogic.natT;

(* Allowed Consts in formulae for presburger tactic*)

val allowed_consts =
  [("All", (iT --> bT) --> bT),
   ("Ex", (iT --> bT) --> bT),
   ("All", (nT --> bT) --> bT),
   ("Ex", (nT --> bT) --> bT),

   ("op &", bT --> bT --> bT),
   ("op |", bT --> bT --> bT),
   ("op -->", bT --> bT --> bT),
   ("op =", bT --> bT --> bT),
   ("Not", bT --> bT),

   ("op <=", iT --> iT --> bT),
   ("op =", iT --> iT --> bT),
   ("op <", iT --> iT --> bT),
   ("Divides.op dvd", iT --> iT --> bT),
   ("Divides.op div", iT --> iT --> iT),
   ("Divides.op mod", iT --> iT --> iT),
   ("op +", iT --> iT --> iT),
   ("op -", iT --> iT --> iT),
   ("op *", iT --> iT --> iT), 
   ("HOL.abs", iT --> iT),
   ("uminus", iT --> iT),
   ("HOL.max", iT --> iT --> iT),
   ("HOL.min", iT --> iT --> iT),

   ("op <=", nT --> nT --> bT),
   ("op =", nT --> nT --> bT),
   ("op <", nT --> nT --> bT),
   ("Divides.op dvd", nT --> nT --> bT),
   ("Divides.op div", nT --> nT --> nT),
   ("Divides.op mod", nT --> nT --> nT),
   ("op +", nT --> nT --> nT),
   ("op -", nT --> nT --> nT),
   ("op *", nT --> nT --> nT), 
   ("Suc", nT --> nT),
   ("HOL.max", nT --> nT --> nT),
   ("HOL.min", nT --> nT --> nT),

   ("Numeral.bin.Bit", binT --> bT --> binT),
   ("Numeral.bin.Pls", binT),
   ("Numeral.bin.Min", binT),
   ("Numeral.number_of", binT --> iT),
   ("Numeral.number_of", binT --> nT),
   ("0", nT),
   ("0", iT),
   ("1", nT),
   ("1", iT),

   ("False", bT),
   ("True", bT)];

(*returns true if the formula is relevant for presburger arithmetic tactic*)
fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
  map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
  subset [iT, nT];

(* Preparation of the formula to be sent to the Integer quantifier *)
(* elimination procedure                                           *)
(* Transforms meta implications and meta quantifiers to object     *)
(* implications and object quantifiers                             *)

fun prepare_for_presburger q fm = 
  let
    val ps = Logic.strip_params fm
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
    val _ = if relevant (rev ps) c then () else raise CooperDec.COOPER
    fun mk_all ((s, T), (P,n)) =
      if 0 mem loose_bnos P then
        (HOLogic.all_const T $ Abs (s, T, P), n)
      else (incr_boundvars ~1 P, n-1)
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
    val (rhs,irhs) = partition (relevant (rev ps)) hs
    val np = length ps
    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
      (ps,(foldr HOLogic.mk_imp (rhs, c), np))
    val (vs, _) = partition (fn t => q orelse (type_of t) = nT)
      (term_frees fm' @ term_vars fm');
    val fm2 = foldr mk_all2 (vs, fm')
  in (fm2, np + length vs, length rhs) end;

(*Object quantifier to meta --*)
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;

(* object implication to meta---*)
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;

(* the presburger tactic*)
fun presburger_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
  let
    val g = BasisLibrary.List.nth (prems_of st, i - 1);
    val sg = sign_of_thm st;
    (* Transform the term*)
    val (t,np,nh) = prepare_for_presburger q g
    (* Some simpsets for dealing with mod div abs and nat*)

    val simpset0 = HOL_basic_ss
      addsimps [mod_div_equality', Suc_plus1]
      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
    (* Simp rules for changing (n::int) to int n *)
    val simpset1 = HOL_basic_ss
      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
      addsplits [zdiff_int_split]
    (*simp rules for elimination of int n*)

    val simpset2 = HOL_basic_ss
      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
      addcongs [conj_le_cong, imp_le_cong]
    (* simp rules for elimination of abs *)

    val simpset3 = HOL_basic_ss addsplits [abs_split]
	      
    val ct = cterm_of sg (HOLogic.mk_Trueprop t)

    (* Theorem for the nat --> int transformation *)
    val pre_thm = Seq.hd (EVERY
      [simp_tac simpset0 i,
       TRY (simp_tac simpset1 i), TRY (simp_tac simpset2 i),
       TRY (simp_tac simpset3 i), TRY (simp_tac presburger_ss i)]
      (trivial ct))

    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i);

    (* The result of the quantifier elimination *)
    val (th, tac) = case (prop_of pre_thm) of
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
          (trace_msg ("calling procedure with term:\n" ^
             Sign.string_of_term sg t1);
           ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
      | _ => (pre_thm, assm_tac i)
  in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);

fun presburger_args meth =
  Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)
    (fn q => fn _ => meth q 1);

fun presburger_method q i = Method.METHOD (fn facts =>
  Method.insert_tac facts 1 THEN presburger_tac q i)

val setup =
  [Method.add_method ("presburger",
     presburger_args presburger_method,
     "decision procedure for Presburger arithmetic"),
   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
     {splits = splits, inj_consts = inj_consts, discrete = discrete,
      presburger = Some (presburger_tac true)})];

end;

val presburger_tac = Presburger.presburger_tac true;