author nipkow Tue, 21 Sep 1999 14:16:08 +0200 changeset 7551 8e934d1a9ac6 parent 7550 060f9954f73d child 7552 0d6d1f50b86d
Now distinguishes discrete from non-distrete types.
```--- 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)

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(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(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;

(*```