Now distinguishes discrete from non-distrete types.
authornipkow
Tue Sep 21 14:16:08 1999 +0200 (1999-09-21)
changeset 75518e934d1a9ac6
parent 7550 060f9954f73d
child 7552 0d6d1f50b86d
Now distinguishes discrete from non-distrete types.
src/Provers/Arith/fast_lin_arith.ML
     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  (*