src/Provers/Arith/fast_lin_arith.ML

   (*preprocessing, performed on a representation of subgoals as list of premises:*)
   val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list
 
   (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
   val pre_tac: Proof.context -> int -> tactic
-  val number_of: IntInf.int * typ -> term
+  val number_of: int * typ -> term
 
   (*the limit on the number of ~= allowed; because each ~= is split
     into two cases, this can lead to an explosion*)
   val fast_arith_neq_limit: int Config.T
 end;

                 | Nat of int (* index of atom *)
                 | LessD of injust
                 | NotLessD of injust
                 | NotLeD of injust
                 | NotLeDD of injust
-                | Multiplied of IntInf.int * injust
-                | Multiplied2 of IntInf.int * injust
+                | Multiplied of int * injust
+                | Multiplied2 of int * injust
                 | Added of injust * injust;
 
-datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust;
+datatype lineq = Lineq of int * lineq_type * int list * injust;
 
 (* ------------------------------------------------------------------------- *)
 (* Finding a (counter) example from the trace of a failed elimination        *)
 (* ------------------------------------------------------------------------- *)
 (* Examples are represented as rational numbers,                             *)

 fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)]
   | elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)]
   | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
 
 (* PRE: ex[v] must be 0! *)
-fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) =
+fun eval ex v (a, le, cs) =
   let
     val rs = map Rat.rat_of_int cs;
     val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
   in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end;
 (* If nth rs v < 0, le should be negated.

 fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l;
 
 fun is_answer (ans as Lineq(k,ty,l,_)) =
   case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
 
-fun calc_blowup (l:IntInf.int list) =
+fun calc_blowup l =
   let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
-  in (length p) * (length n) end;
+  in length p * length n end;
 
 (* ------------------------------------------------------------------------- *)
 (* Main elimination code:                                                    *)
 (*                                                                           *)
 (* (1) Looks for immediate solutions (false assertions with no variables).   *)

   in extract [] end;
 
 fun print_ineqs ineqs =
   if !trace then
      tracing(cat_lines(""::map (fn Lineq(c,t,l,_) =>
-       IntInf.toString c ^
+       string_of_int c ^
        (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
-       commas(map IntInf.toString l)) ineqs))
+       commas(map string_of_int l)) ineqs))
   else ();
 
 type history = (int * lineq list) list;
 datatype result = Success of injust | Failure of history;
 

   if null nontriv then Failure hist
   else
   let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
   if not (null eqs) then
      let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
-         val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
+         val sclist = sort (fn (x,y) => int_ord (abs x, abs y))
                            (List.filter (fn i => i<>0) clist)
          val c = hd sclist
          val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
                extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
          val v = find_index_eq c ceq

         | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
         | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
         | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
         | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
         | mk (Added (j1, j2))     = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
-        | mk (Multiplied (n, j))  = (trace_msg ("*" ^ IntInf.toString n); trace_thm "*" (multn (n, mk j)))
-        | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ IntInf.toString n); trace_thm "**" (multn2 (n, mk j)))
+        | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
+        | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
 
   in trace_msg "mkthm";
      let val thm = trace_thm "Final thm:" (mk just)
      in let val fls = simplify simpset' thm
         in trace_thm "After simplification:" fls;

      end handle FalseE thm => trace_thm "False reached early:" thm
   end
 end;
 
 fun coeff poly atom =
-  AList.lookup (op aconv) poly atom |> the_default (0: integer);
-
-fun lcms ks = fold Integer.lcm ks 1;
+  AList.lookup (op aconv) poly atom |> the_default 0;
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
-    val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
+    val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
     fun mult(t,r) =
         let val (i,j) = Rat.quotient_of_rat r
         in (t,i * (m div j)) end
 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
 

 (* Print (counter) example                                                   *)
 (* ------------------------------------------------------------------------- *)
 
 fun print_atom((a,d),r) =
   let val (p,q) = Rat.quotient_of_rat r
-      val s = if d then IntInf.toString p else
+      val s = if d then string_of_int p else
               if p = 0 then "0"
-              else IntInf.toString p ^ "/" ^ IntInf.toString q
+              else string_of_int p ^ "/" ^ string_of_int q
   in a ^ " = " ^ s end;
 
 fun produce_ex sds =
   curry (op ~~) sds
   #> map print_atom