# HG changeset patch # User nipkow # Date 1118419152 -7200 # Node ID 2e2a506553a3b701c2a4f6c313bf7c3fdc0b2241 # Parent f1275d2a1deed16b48a51e298f4a895747c949af IntInf change diff -r f1275d2a1dee -r 2e2a506553a3 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Fri Jun 10 16:15:36 2005 +0200 +++ b/src/HOL/arith_data.ML Fri Jun 10 17:59:12 2005 +0200 @@ -363,8 +363,7 @@ let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg in decomp2 (sg,discrete,inj_consts) end -(*FIXME: remove the IntInf.fromInt when linear arithmetic is converted to IntInfs*) -fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin (IntInf.fromInt n)) +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n) end; diff -r f1275d2a1dee -r 2e2a506553a3 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Jun 10 16:15:36 2005 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jun 10 17:59:12 2005 +0200 @@ -15,8 +15,6 @@ Only take premises and conclusions into account that are already (negated) (in)equations. lin_arith_prover tries to prove or disprove the term. - -FIXME: convert to IntInf.int throughout. *) (* Debugging: set Fast_Arith.trace *) @@ -55,7 +53,7 @@ sig val decomp: Sign.sg -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option - val number_of: int * typ -> term + val number_of: IntInf.int * typ -> term end; (* decomp(`x Rel y') should yield (p,i,Rel,q,j,d) @@ -141,11 +139,11 @@ | NotLessD of injust | NotLeD of injust | NotLeDD of injust - | Multiplied of int * injust - | Multiplied2 of int * injust + | Multiplied of IntInf.int * injust + | Multiplied2 of IntInf.int * injust | Added of injust * injust; -datatype lineq = Lineq of int * lineq_type * int list * injust; +datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust; fun el 0 (h::_) = h | el n (_::t) = el (n - 1) t @@ -171,10 +169,10 @@ val rat0 = rat_of_int 0; (* PRE: ex[v] must be 0! *) -fun eval (ex:rat list) v (a:int,le,cs:int list) = - let val rs = map rat_of_int cs +fun eval (ex:rat list) v (a:IntInf.int,le,cs:IntInf.int list) = + let val rs = map rat_of_intinf cs val rsum = Library.foldl ratadd (rat0,map ratmul (rs ~~ ex)) - in (ratmul(ratadd(rat_of_int a,ratneg rsum), ratinv(el v rs)), le) end; + in (ratmul(ratadd(rat_of_intinf a,ratneg rsum), ratinv(el v rs)), le) end; (* If el v rs < 0, le should be negated. Instead this swap is taken into account in ratrelmin2. *) @@ -258,7 +256,7 @@ fun findex0 discr n lineqs = let val ineqs = Library.foldl elim_eqns ([],lineqs) - val rineqs = map (fn (a,le,cs) => (rat_of_int a, le, map rat_of_int cs)) + val rineqs = map (fn (a,le,cs) => (rat_of_intinf a, le, map rat_of_intinf cs)) ineqs in pick_vars discr (rineqs,replicate n rat0) end; @@ -301,7 +299,7 @@ fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = let val c1 = el v l1 and c2 = el v l2 - val m = IntInf.toInt (lcm(IntInf.fromInt (abs c1), IntInf.fromInt(abs c2))) + val m = lcm(abs c1, abs c2) val m1 = m div (abs c1) and m2 = m div (abs c2) val (n1,n2) = if (c1 >= 0) = (c2 >= 0) @@ -322,7 +320,7 @@ 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 = +fun calc_blowup (l:IntInf.int list) = let val (p,n) = List.partition (apl(0,op<)) (List.filter (apl(0,op<>)) l) in (length p) * (length n) end; @@ -350,9 +348,9 @@ fun print_ineqs ineqs = if !trace then tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => - string_of_int c ^ + IntInf.toString c ^ (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ - commas(map string_of_int l)) ineqs)) + commas(map IntInf.toString l)) ineqs)) else (); type history = (int * lineq list) list; @@ -371,7 +369,7 @@ 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) => int_ord(abs(x),abs(y))) + val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y))) (List.filter (fn i => i<>0) clist) val c = hd sclist val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) = @@ -478,8 +476,8 @@ | 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("*"^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))) + | 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))) in trace_msg "mkthm"; let val thm = trace_thm "Final thm:" (mk just) @@ -497,16 +495,16 @@ end end; -fun coeff poly atom = case assoc(poly,atom) of NONE => 0 | SOME i => i; +fun coeff poly atom : IntInf.int = + case assoc(poly,atom) of NONE => 0 | SOME i => i; -fun lcms_intinf is = Library.foldl lcm (1, is); -fun lcms is = IntInf.toInt (lcms_intinf (map IntInf.fromInt is)); +fun lcms is = Library.foldl lcm (1, is); fun integ(rlhs,r,rel,rrhs,s,d) = -let val (rn,rd) = pairself IntInf.toInt (rep_rat r) and (sn,sd) = pairself IntInf.toInt (rep_rat s) - val m = IntInf.toInt (lcms_intinf(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs))) +let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s + val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)) fun mult(t,r) = - let val (i,j) = pairself IntInf.toInt (rep_rat r) + let val (i,j) = (rep_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