src/HOL/Tools/Presburger/cooper_dec.ML

   exception COOPER
   exception COOPER_ORACLE of term
   val is_arith_rel : term -> bool
   val mk_numeral : int -> term
   val dest_numeral : term -> int
+  val is_numeral : term -> bool
   val zero : term
   val one : term
   val linear_cmul : int -> term -> term
   val linear_add : string list -> term -> term -> term 
   val linear_sub : string list -> term -> term -> term 

 (* Linearize the atoms in a formula, and eliminate non-strict inequalities.  *) 
 (* ------------------------------------------------------------------------- *) 
  
 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
  
-fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =  
+fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
+    if is_numeral c then   
       let val c' = (mk_numeral(abs(dest_numeral c)))  
       in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) 
       end 
+    else (warning "Nonlinear term --- Non numeral leftside at dvd"
+      ;raise COOPER)
   |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
   |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   |linform vars  (Const("op <=",_)$ s $ t ) = 
         (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))