author nipkow Tue Sep 21 14:16:08 1999 +0200 (1999-09-21) changeset 7551 8e934d1a9ac6 parent 7550 060f9954f73d child 7552 0d6d1f50b86d
Now distinguishes discrete from non-distrete types.
```     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 21 14:14:14 1999 +0200
1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 21 14:16:08 1999 +0200
1.3 @@ -54,15 +54,16 @@
1.4                              (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
1.5    val lessD:            thm list ref (* m < n ==> m+1 <= n *)
1.6    val decomp:
1.7 -    (term -> ((term * int)list * int * string * (term * int)list * int)option)
1.8 -    ref
1.9 +    term ->
1.10 +      ((term * int)list * int * string * (term * int)list * int * bool)option
1.11    val simp: (thm -> thm) ref
1.12  end;
1.13  (*
1.14 -decomp(`x Rel y') should yield (p,i,Rel,q,j)
1.15 +decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
1.16     where Rel is one of "<", "~<", "<=", "~<=" and "=" and
1.17           p/q is the decomposition of the sum terms x/y into a list
1.18 -         of summand * multiplicity pairs and a constant summand.
1.19 +         of summand * multiplicity pairs and a constant summand and
1.20 +         d indicates if the domain is discrete.
1.21
1.22  simp must reduce contradictory <= to False.
1.23     It should also cancel common summands to keep <= reduced;
1.24 @@ -94,6 +95,7 @@
1.25                  | LessD of injust
1.26                  | NotLessD of injust
1.27                  | NotLeD of injust
1.28 +                | NotLeDD of injust
1.29                  | Multiplied of int * injust
1.30                  | Added of injust * injust;
1.31
1.32 @@ -191,13 +193,13 @@
1.33          | extract xs []      = (None,xs)
1.34    in extract [] end;
1.35
1.36 -(*
1.37 +
1.38  fun print_ineqs ineqs =
1.39   writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
1.40     string_of_int c ^
1.41     (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
1.42     commas(map string_of_int l)) ineqs));
1.43 -*)
1.44 +
1.45
1.46  fun elim ineqs =
1.47    let (*val dummy = print_ineqs ineqs;*)
1.48 @@ -251,9 +253,9 @@
1.49   exception FalseE of thm
1.50  in
1.51  fun mkthm sg asms just =
1.52 -  let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_)) =>
1.53 +  let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
1.54                              map fst lhs  union  (map fst rhs  union  ats))
1.55 -                        ([], mapfilter (!LA_Data.decomp o concl_of) asms)
1.56 +                        ([], mapfilter (LA_Data.decomp o concl_of) asms)
1.57
1.58        fun addthms thm1 thm2 =
1.59          let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
1.60 @@ -269,22 +271,23 @@
1.61          let val thm' = !LA_Data.simp thm
1.62          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
1.63
1.64 -      fun mk(Asm i) = nth_elem(i,asms)
1.65 -        | mk(Nat(i)) = LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))
1.66 -        | mk(LessD(j)) = hd([mk j] RL !LA_Data.lessD)
1.67 -        | mk(NotLeD(j)) = hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)
1.68 -        | mk(NotLessD(j)) = mk j RS LA_Logic.not_lessD
1.69 -        | mk(Added(j1,j2)) = simp(addthms (mk j1) (mk j2))
1.70 -        | mk(Multiplied(n,j)) = multn(n,mk j)
1.71 +      fun mk(Asm i) = ((*writeln"Asm";prth*)(nth_elem(i,asms)))
1.72 +        | mk(Nat(i)) = ((*writeln"N";LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
1.73 +        | mk(LessD(j)) = ((*writeln"L";prth*)(hd([mk j] RL !LA_Data.lessD)))
1.74 +        | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD))
1.75 +        | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
1.76 +        | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD))
1.77 +        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp(prth(addthms (mk j1) (mk j2)))))
1.78 +        | mk(Multiplied(n,j)) = ((*writeln"*";multn(n,mk j))
1.79
1.80 -  in !LA_Data.simp(mk just) handle FalseE thm => thm end
1.81 +  in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end
1.82  end;
1.83
1.84  fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i;
1.85
1.86  fun mklineq atoms =
1.87    let val n = length atoms in
1.88 -    fn ((lhs,i,rel,rhs,j),k) =>
1.89 +    fn ((lhs,i,rel,rhs,j,discrete),k) =>
1.90      let val lhsa = map (coeff lhs) atoms
1.91          and rhsa = map (coeff rhs) atoms
1.92          val diff = map2 (op -) (rhsa,lhsa)
1.93 @@ -292,8 +295,12 @@
1.94          val just = Asm k
1.95      in case rel of
1.96          "<="   => Some(Lineq(c,Le,diff,just))
1.97 -       | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,NotLeD(just)))
1.98 -       | "<"   => Some(Lineq(c+1,Le,diff,LessD(just)))
1.99 +       | "~<=" => if discrete
1.100 +                  then Some(Lineq(1-c,Le,map (op ~) diff,NotLeDD(just)))
1.101 +                  else Some(Lineq(~c,Lt,map (op ~) diff,NotLeD(just)))
1.102 +       | "<"   => if discrete
1.103 +                  then Some(Lineq(c+1,Le,diff,LessD(just)))
1.104 +                  else Some(Lineq(c,Lt,diff,just))
1.105         | "~<"  => Some(Lineq(~c,Le,map (op~) diff,NotLessD(just)))
1.106         | "="   => Some(Lineq(c,Eq,diff,just))
1.107         | "~="  => None
1.108 @@ -308,7 +315,7 @@
1.109    else None
1.110
1.111  fun abstract pTs items =
1.112 -  let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_),_)) =>
1.113 +  let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_,_),_)) =>
1.114                              (map fst lhs) union ((map fst rhs) union ats))
1.115                          ([],items)
1.116        val ixs = 0 upto (length(atoms)-1)
1.117 @@ -330,11 +337,11 @@
1.118      state;
1.119
1.120  (* Double refutation caused by equality in conclusion *)
1.121 -fun refute2(pTs,items, (rhs,i,_,lhs,j), nHs) =
1.122 -  (case elim (abstract pTs (items@[((rhs,i,"<",lhs,j),nHs)])) of
1.123 +fun refute2(pTs,items, (rhs,i,_,lhs,j,d), nHs) =
1.124 +  (case elim (abstract pTs (items@[((rhs,i,"<",lhs,j,d),nHs)])) of
1.125      None => []
1.126    | Some(Lineq(_,_,_,j1)) =>
1.127 -      (case elim (abstract pTs (items@[((lhs,j,"<",rhs,i),nHs)])) of
1.128 +      (case elim (abstract pTs (items@[((lhs,j,"<",rhs,i,d),nHs)])) of
1.129          None => []
1.130        | Some(Lineq(_,_,_,j2)) => [j1,j2]));
1.131
1.132 @@ -350,16 +357,16 @@
1.133  fun prove(pTs,Hs,concl) =
1.134  let val nHs = length Hs
1.135      val ixHs = Hs ~~ (0 upto (nHs-1))
1.136 -    val Hitems = mapfilter (fn (h,i) => case !LA_Data.decomp h of
1.137 +    val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of
1.138                                   None => None | Some(it) => Some(it,i)) ixHs
1.139 -in case !LA_Data.decomp concl of
1.140 +in case LA_Data.decomp concl of
1.141       None => if null Hitems then [] else refute1(pTs,Hitems)
1.142 -   | Some(citem as (r,i,rel,l,j)) =>
1.143 +   | Some(citem as (r,i,rel,l,j,d)) =>
1.144         if rel = "="
1.145         then refute2(pTs,Hitems,citem,nHs)
1.146         else let val neg::rel0 = explode rel
1.147                  val nrel = if neg = "~" then implode rel0 else "~"^rel
1.148 -            in refute1(pTs, Hitems@[((r,i,nrel,l,j),nHs)]) end
1.149 +            in refute1(pTs, Hitems@[((r,i,nrel,l,j,d),nHs)]) end
1.150  end;
1.151
1.152  (*
```