# HG changeset patch # User nipkow # Date 937916168 -7200 # Node ID 8e934d1a9ac6221f925fcfe3a2014e981b1f4373 # Parent 060f9954f73d3decdfc2a9a96e9ddd63e202e028 Now distinguishes discrete from non-distrete types. diff -r 060f9954f73d -r 8e934d1a9ac6 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 21 14:14:14 1999 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 21 14:16:08 1999 +0200 @@ -54,15 +54,16 @@ (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *) val lessD: thm list ref (* m < n ==> m+1 <= n *) val decomp: - (term -> ((term * int)list * int * string * (term * int)list * int)option) - ref + term -> + ((term * int)list * int * string * (term * int)list * int * bool)option val simp: (thm -> thm) ref end; (* -decomp(`x Rel y') should yield (p,i,Rel,q,j) +decomp(`x Rel y') should yield (p,i,Rel,q,j,d) where Rel is one of "<", "~<", "<=", "~<=" and "=" and p/q is the decomposition of the sum terms x/y into a list - of summand * multiplicity pairs and a constant summand. + of summand * multiplicity pairs and a constant summand and + d indicates if the domain is discrete. simp must reduce contradictory <= to False. It should also cancel common summands to keep <= reduced; @@ -94,6 +95,7 @@ | LessD of injust | NotLessD of injust | NotLeD of injust + | NotLeDD of injust | Multiplied of int * injust | Added of injust * injust; @@ -191,13 +193,13 @@ | extract xs [] = (None,xs) in extract [] end; -(* + fun print_ineqs ineqs = writeln(cat_lines(""::map (fn Lineq(c,t,l,_) => string_of_int c ^ (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ commas(map string_of_int l)) ineqs)); -*) + fun elim ineqs = let (*val dummy = print_ineqs ineqs;*) @@ -251,9 +253,9 @@ exception FalseE of thm in fun mkthm sg asms just = - let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_)) => + let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) => map fst lhs union (map fst rhs union ats)) - ([], mapfilter (!LA_Data.decomp o concl_of) asms) + ([], mapfilter (LA_Data.decomp o concl_of) asms) fun addthms thm1 thm2 = let val conj = thm1 RS (thm2 RS LA_Logic.conjI) @@ -269,22 +271,23 @@ let val thm' = !LA_Data.simp thm in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end - fun mk(Asm i) = nth_elem(i,asms) - | mk(Nat(i)) = LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)) - | mk(LessD(j)) = hd([mk j] RL !LA_Data.lessD) - | mk(NotLeD(j)) = hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD) - | mk(NotLessD(j)) = mk j RS LA_Logic.not_lessD - | mk(Added(j1,j2)) = simp(addthms (mk j1) (mk j2)) - | mk(Multiplied(n,j)) = multn(n,mk j) + fun mk(Asm i) = ((*writeln"Asm";prth*)(nth_elem(i,asms))) + | mk(Nat(i)) = ((*writeln"N";LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) + | mk(LessD(j)) = ((*writeln"L";prth*)(hd([mk j] RL !LA_Data.lessD))) + | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD)) + | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD))) + | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD)) + | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp(prth(addthms (mk j1) (mk j2))))) + | mk(Multiplied(n,j)) = ((*writeln"*";multn(n,mk j)) - in !LA_Data.simp(mk just) handle FalseE thm => thm end + in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end end; fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i; fun mklineq atoms = let val n = length atoms in - fn ((lhs,i,rel,rhs,j),k) => + fn ((lhs,i,rel,rhs,j,discrete),k) => let val lhsa = map (coeff lhs) atoms and rhsa = map (coeff rhs) atoms val diff = map2 (op -) (rhsa,lhsa) @@ -292,8 +295,12 @@ val just = Asm k in case rel of "<=" => Some(Lineq(c,Le,diff,just)) - | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,NotLeD(just))) - | "<" => Some(Lineq(c+1,Le,diff,LessD(just))) + | "~<=" => if discrete + then Some(Lineq(1-c,Le,map (op ~) diff,NotLeDD(just))) + else Some(Lineq(~c,Lt,map (op ~) diff,NotLeD(just))) + | "<" => if discrete + then Some(Lineq(c+1,Le,diff,LessD(just))) + else Some(Lineq(c,Lt,diff,just)) | "~<" => Some(Lineq(~c,Le,map (op~) diff,NotLessD(just))) | "=" => Some(Lineq(c,Eq,diff,just)) | "~=" => None @@ -308,7 +315,7 @@ else None fun abstract pTs items = - let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_),_)) => + let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_,_),_)) => (map fst lhs) union ((map fst rhs) union ats)) ([],items) val ixs = 0 upto (length(atoms)-1) @@ -330,11 +337,11 @@ state; (* Double refutation caused by equality in conclusion *) -fun refute2(pTs,items, (rhs,i,_,lhs,j), nHs) = - (case elim (abstract pTs (items@[((rhs,i,"<",lhs,j),nHs)])) of +fun refute2(pTs,items, (rhs,i,_,lhs,j,d), nHs) = + (case elim (abstract pTs (items@[((rhs,i,"<",lhs,j,d),nHs)])) of None => [] | Some(Lineq(_,_,_,j1)) => - (case elim (abstract pTs (items@[((lhs,j,"<",rhs,i),nHs)])) of + (case elim (abstract pTs (items@[((lhs,j,"<",rhs,i,d),nHs)])) of None => [] | Some(Lineq(_,_,_,j2)) => [j1,j2])); @@ -350,16 +357,16 @@ fun prove(pTs,Hs,concl) = let val nHs = length Hs val ixHs = Hs ~~ (0 upto (nHs-1)) - val Hitems = mapfilter (fn (h,i) => case !LA_Data.decomp h of + val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of None => None | Some(it) => Some(it,i)) ixHs -in case !LA_Data.decomp concl of +in case LA_Data.decomp concl of None => if null Hitems then [] else refute1(pTs,Hitems) - | Some(citem as (r,i,rel,l,j)) => + | Some(citem as (r,i,rel,l,j,d)) => if rel = "=" then refute2(pTs,Hitems,citem,nHs) else let val neg::rel0 = explode rel val nrel = if neg = "~" then implode rel0 else "~"^rel - in refute1(pTs, Hitems@[((r,i,nrel,l,j),nHs)]) end + in refute1(pTs, Hitems@[((r,i,nrel,l,j,d),nHs)]) end end; (*