# HG changeset patch # User haftmann # Date 1129898944 -7200 # Node ID ff954cc338c796be80d7f9248d8fcdb59813bdee # Parent 924d3e71cdc9d0e72dba5881473627ac6094f0ec introduced functions from Pure/General/rat.ML diff -r 924d3e71cdc9 -r ff954cc338c7 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Fri Oct 21 14:47:37 2005 +0200 +++ b/src/HOL/arith_data.ML Fri Oct 21 14:49:04 2005 +0200 @@ -243,13 +243,13 @@ | nT _ = false; fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) - | SOME n => (AList.update (op =) (t, ratadd (n, m)) p, i)); + | SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i)); exception Zero; -fun rat_of_term(numt,dent) = +fun rat_of_term (numt,dent) = let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent - in if den = 0 then raise Zero else int_ratdiv(num,den) end; + in if den = 0 then raise Zero else Rat.rat_of_quotient (num,den) end; (* Warning: in rare cases number_of encloses a non-numeral, in which case dest_binum raises TERM; hence all the handles below. @@ -269,29 +269,29 @@ let fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of Const("Numeral.number_of",_)$n - => demult(t,ratmul(m,rat_of_intinf(HOLogic.dest_binum n))) + => demult(t,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) | Const("uminus",_)$(Const("Numeral.number_of",_)$n) - => demult(t,ratmul(m,rat_of_intinf(~(HOLogic.dest_binum n)))) + => demult(t,Rat.mult(m,Rat.rat_of_intinf(~(HOLogic.dest_binum n)))) | Const("Suc",_) $ _ - => demult(t,ratmul(m,rat_of_int(number_of_Sucs s))) + => demult(t,Rat.mult(m,Rat.rat_of_int(number_of_Sucs s))) | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m) | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) => let val den = HOLogic.dest_binum dent in if den = 0 then raise Zero - else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_intinf den))) + else demult(mC $ numt $ t,Rat.mult(m, Rat.inv(Rat.rat_of_intinf den))) end | _ => atomult(mC,s,t,m) ) handle TERM _ => atomult(mC,s,t,m)) | demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) = (let val den = HOLogic.dest_binum dent - in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_intinf den))) end + in if den = 0 then raise Zero else demult(t,Rat.mult(m, Rat.inv(Rat.rat_of_intinf den))) end handle TERM _ => (SOME atom,m)) - | demult(Const("0",_),m) = (NONE, rat_of_int 0) + | demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0) | demult(Const("1",_),m) = (NONE, m) | demult(t as Const("Numeral.number_of",_)$n,m) = - ((NONE,ratmul(m,rat_of_intinf(HOLogic.dest_binum n))) + ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) handle TERM _ => (SOME t,m)) - | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1))) + | demult(Const("uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1))) | demult(t as Const f $ x, m) = (if f mem inj_consts then SOME x else SOME t,m) | demult(atom,m) = (SOME atom,m) @@ -305,29 +305,29 @@ (* Turn term into list of summand * multiplicity plus a constant *) fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) | poly(all as Const("op -",T) $ s $ t, m, pi) = - if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,ratneg m,pi)) + if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi)) | poly(all as Const("uminus",T) $ t, m, pi) = - if nT T then add_atom(all,m,pi) else poly(t,ratneg m,pi) + if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi) | poly(Const("0",_), _, pi) = pi - | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m)) - | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m))) + | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m)) + | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m))) | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) = (case demult inj_consts (t,m) of - (NONE,m') => (p,ratadd(i,m)) + (NONE,m') => (p,Rat.add(i,m)) | (SOME u,m') => add_atom(u,m',pi)) | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) = (case demult inj_consts (t,m) of - (NONE,m') => (p,ratadd(i,m')) + (NONE,m') => (p,Rat.add(i,m')) | (SOME u,m') => add_atom(u,m',pi)) | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) = - ((p,ratadd(i,ratmul(m,rat_of_intinf(HOLogic.dest_binum t)))) + ((p,Rat.add(i,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum t)))) handle TERM _ => add_atom all) | poly(all as Const f $ x, m, pi) = if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi) | poly x = add_atom x; -val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0)) -and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0)) +val (p,i) = poly(lhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0)) +and (q,j) = poly(rhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0)) in case rel of "op <" => SOME(p,i,"<",q,j) diff -r 924d3e71cdc9 -r ff954cc338c7 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Oct 21 14:47:37 2005 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Oct 21 14:49:04 2005 +0200 @@ -53,7 +53,7 @@ signature LIN_ARITH_DATA = sig val decomp: - theory -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option + theory -> term -> ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool) option val number_of: IntInf.int * typ -> term end; (* @@ -168,49 +168,43 @@ | elim_eqns(ineqs,Lineq(i,Lt,cs,_)) = (i,false,cs)::ineqs; (* PRE: ex[v] must be 0! *) -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_intinf a,ratneg rsum), ratinv(el v rs)), le) end; +fun eval (ex:Rat.rat list) v (a:IntInf.int,le,cs:IntInf.int list) = + let val rs = map Rat.rat_of_intinf cs + val rsum = Library.foldl Rat.add (Rat.zero, map Rat.mult (rs ~~ ex)) + in (Rat.mult (Rat.add(Rat.rat_of_intinf a,Rat.neg rsum), Rat.inv(el v rs)), le) end; (* If el v rs < 0, le should be negated. Instead this swap is taken into account in ratrelmin2. *) fun ratrelmin2(x as (r,ler),y as (s,les)) = - if r=s then (r, (not ler) andalso (not les)) else if ratle(r,s) then x else y; + if r=s then (r, (not ler) andalso (not les)) else if Rat.le(r,s) then x else y; fun ratrelmax2(x as (r,ler),y as (s,les)) = - if r=s then (r,ler andalso les) else if ratle(r,s) then y else x; + if r=s then (r,ler andalso les) else if Rat.le(r,s) then y else x; val ratrelmin = foldr1 ratrelmin2; val ratrelmax = foldr1 ratrelmax2; -fun ratroundup r = let val (p,q) = rep_rat r - in if q=1 then r else rat_of_intinf((p div q) + 1) end - -fun ratrounddown r = let val (p,q) = rep_rat r - in if q=1 then r else rat_of_intinf((p div q) - 1) end - fun ratexact up (r,exact) = if exact then r else - let val (p,q) = rep_rat r - val nth = ratinv(rat_of_intinf q) - in ratadd(r,if up then nth else ratneg nth) end; + let val (p,q) = Rat.quotient_of_rat r + val nth = Rat.inv(Rat.rat_of_intinf q) + in Rat.add(r,if up then nth else Rat.neg nth) end; -fun ratmiddle(r,s) = ratmul(ratadd(r,s),ratinv(rat_of_int 2)); +fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2)); fun choose2 d ((lb,exactl),(ub,exactu)) = - if ratle(lb,rat0) andalso (lb <> rat0 orelse exactl) andalso - ratle(rat0,ub) andalso (ub <> rat0 orelse exactu) - then rat0 else + if Rat.le(lb,Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso + Rat.le(Rat.zero,ub) andalso (ub <> Rat.zero orelse exactu) + then Rat.zero else if not d - then (if ratge0 lb + then (if Rat.ge0 lb then if exactl then lb else ratmiddle(lb,ub) else if exactu then ub else ratmiddle(lb,ub)) else (* discrete domain, both bounds must be exact *) - if ratge0 lb then let val lb' = ratroundup lb - in if ratle(lb',ub) then lb' else raise NoEx end - else let val ub' = ratrounddown ub - in if ratle(lb,ub') then ub' else raise NoEx end; + if Rat.ge0 lb then let val lb' = Rat.roundup lb + in if Rat.le(lb',ub) then lb' else raise NoEx end + else let val ub' = Rat.rounddown ub + in if Rat.le(lb,ub') then ub' else raise NoEx end; fun findex1 discr (ex,(v,lineqs)) = let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs; @@ -223,28 +217,28 @@ fun findex discr = Library.foldl (findex1 discr); fun elim1 v x = - map (fn (a,le,bs) => (ratadd(a,ratneg(ratmul(el v bs,x))), le, - nth_update rat0 (v,bs))); + map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le, + nth_update Rat.zero (v,bs))); -fun single_var v (_,_,cs) = (filter_out (equal rat0) cs = [el v cs]); +fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]); (* The base case: all variables occur only with positive or only with negative coefficients *) fun pick_vars discr (ineqs,ex) = - let val nz = filter_out (fn (_,_,cs) => forall (equal rat0) cs) ineqs + let val nz = filter_out (fn (_,_,cs) => forall (equal Rat.zero) cs) ineqs in case nz of [] => ex | (_,_,cs) :: _ => - let val v = find_index (not o equal rat0) cs + let val v = find_index (not o equal Rat.zero) cs val d = List.nth(discr,v) - val pos = ratge0(el v cs) + val pos = Rat.ge0(el v cs) val sv = List.filter (single_var v) nz val minmax = - if pos then if d then ratroundup o fst o ratrelmax + if pos then if d then Rat.roundup o fst o ratrelmax else ratexact true o ratrelmax - else if d then ratrounddown o fst o ratrelmin + else if d then Rat.rounddown o fst o ratrelmin else ratexact false o ratrelmin - val bnds = map (fn (a,le,bs) => (ratmul(a,ratinv(el v bs)),le)) sv - val x = minmax((rat0,if pos then true else false)::bnds) + val bnds = map (fn (a,le,bs) => (Rat.mult(a,Rat.inv(el v bs)),le)) sv + val x = minmax((Rat.zero,if pos then true else false)::bnds) val ineqs' = elim1 v x nz val ex' = nth_update x (v,ex) in pick_vars discr (ineqs',ex') end @@ -252,9 +246,9 @@ fun findex0 discr n lineqs = let val ineqs = Library.foldl elim_eqns ([],lineqs) - val rineqs = map (fn (a,le,cs) => (rat_of_intinf a, le, map rat_of_intinf cs)) + val rineqs = map (fn (a,le,cs) => (Rat.rat_of_intinf a, le, map Rat.rat_of_intinf cs)) ineqs - in pick_vars discr (rineqs,replicate n rat0) end; + in pick_vars discr (rineqs,replicate n Rat.zero) end; (* ------------------------------------------------------------------------- *) (* End of counter example finder. The actual decision procedure starts here. *) @@ -498,10 +492,10 @@ fun lcms is = Library.foldl lcm (1, is); fun integ(rlhs,r,rel,rrhs,s,d) = -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)) +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)) fun mult(t,r) = - let val (i,j) = (rep_rat 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 @@ -532,7 +526,7 @@ (* ------------------------------------------------------------------------- *) fun print_atom((a,d),r) = - let val (p,q) = rep_rat r + let val (p,q) = Rat.quotient_of_rat r val s = if d then IntInf.toString p else if p = 0 then "0" else IntInf.toString p ^ "/" ^ IntInf.toString q @@ -551,7 +545,7 @@ fun s_of_t t = Sign.string_of_term sg (subst_bounds(frees,t)); val (v,lineqs) :: hist' = hist val start = if v = ~1 then (findex0 discr n lineqs,hist') - else (replicate n rat0,hist) + else (replicate n Rat.zero,hist) in warning "arith failed - see trace for a counter example"; print_ex ((map s_of_t atoms)~~discr) (findex discr start) handle NoEx =>