1(*****************************************************************************)
2(* FILE          : norm_ineqs.sml                                            *)
3(* DESCRIPTION   : Functions for normalizing inequalities.                   *)
4(*                                                                           *)
5(* READS FILES   : <none>                                                    *)
6(* WRITES FILES  : <none>                                                    *)
7(*                                                                           *)
8(* AUTHOR        : R.J.Boulton, University of Cambridge                      *)
9(* DATE          : 4th March 1991                                            *)
10(*                                                                           *)
11(* TRANSLATOR    : R.J.Boulton, University of Cambridge                      *)
12(* DATE          : 5th February 1993                                         *)
13(*                                                                           *)
14(* LAST MODIFIED : R.J.Boulton                                               *)
15(* DATE          : 7th August 1996                                           *)
16(*****************************************************************************)
17
18structure Norm_ineqs :> Norm_ineqs =
19struct
20
21
22open Arbint HolKernel Arith_cons RJBConv
23     Term_coeffs Thm_convs Norm_bool Norm_arith;
24
25infix THENC <<;
26
27val op << = String.<
28
29fun failwith f = raise (mk_HOL_ERR "Norm_ineqs" f "")
30
31
32(*===========================================================================*)
33(* Adding terms to inequalities                                              *)
34(*===========================================================================*)
35
36(*---------------------------------------------------------------------------*)
37(* ADD_TERM_TO_LEQ_CONV : term -> conv                                       *)
38(*                                                                           *)
39(* ADD_TERM_TO_LEQ_CONV `x` `a <= b` returns the theorem:                    *)
40(*                                                                           *)
41(*    |- (a <= b) = ((x + a) <= (x + b))                                     *)
42(*---------------------------------------------------------------------------*)
43
44fun ADD_TERM_TO_LEQ_CONV addition tm =
45 (let val (tm1,tm2) = dest_leq tm
46      val tm' = mk_leq (mk_plus (addition,tm1),mk_plus (addition,tm2))
47  in  SYM (LEQ_PLUS_CONV tm')
48  end
49 ) handle (HOL_ERR _) => failwith "ADD_TERM_TO_LEQ_CONV";
50
51(*---------------------------------------------------------------------------*)
52(* ADD_COEFFS_TO_LEQ_CONV : (int * (string * int) list) -> conv              *)
53(*                                                                           *)
54(* Adds terms to both sides of a less-than-or-equal-to inequality. The       *)
55(* conversion avoids adding a zero constant but does not concern itself with *)
56(* eliminating zero terms in any other way.                                  *)
57(*---------------------------------------------------------------------------*)
58
59fun ADD_COEFFS_TO_LEQ_CONV (const,bind) =
60 let fun add_terms_conv bind =
61        if (null bind)
62        then ALL_CONV
63        else let val (name,coeff) = hd bind
64                 val addition = mk_mult (term_of_int coeff,mk_num_var name)
65             in  ((add_terms_conv (tl bind)) THENC
66                  (ADD_TERM_TO_LEQ_CONV addition))
67             end
68 in fn tm =>
69 (((add_terms_conv bind) THENC
70   (if (const = zero)
71    then ALL_CONV
72    else ADD_TERM_TO_LEQ_CONV (term_of_int const))) tm)
73 handle (HOL_ERR _) => failwith "ADD_COEFFS_TO_LEQ_CONV"
74 end;
75
76(*===========================================================================*)
77(* Normalizing inequalities                                                  *)
78(*===========================================================================*)
79
80(*---------------------------------------------------------------------------*)
81(* LESS_OR_EQ_GATHER_CONV : conv                                             *)
82(*                                                                           *)
83(* Assumes that the argument term is a less-than-or-equal-to of two fully    *)
84(* normalized arithmetic expressions. The conversion transforms such a term  *)
85(* to a less-than-or-equal-to in which each variable occurs on only one side *)
86(* of the inequality, and a constant term appears on at most one side,       *)
87(* unless the whole of one side is zero.                                     *)
88(*                                                                           *)
89(* Here is an example result:                                                *)
90(*                                                                           *)
91(*    |- (1 + ((3 * x) + (1 * z))) <= (2 + ((1 * x) + (4 * y))) =            *)
92(*       ((2 * x) + (1 * z)) <= (1 + (4 * y))                                *)
93(*---------------------------------------------------------------------------*)
94
95val LESS_OR_EQ_GATHER_CONV =
96 let fun subtract_common_terms bind1 bind2 =
97        if (null bind1) then ([],[],bind2)
98        else if (null bind2) then ([],bind1,[])
99        else let val (name1:string,coeff1:int) = hd bind1
100                 and (name2,coeff2) = hd bind2
101             in  if (name1 = name2) then
102                     (let val (c,b1,b2) =
103                             subtract_common_terms (tl bind1) (tl bind2)
104                      in  if (coeff1 = coeff2) then ((name1,coeff1)::c,b1,b2)
105                          else if (coeff1 < coeff2) then
106                             ((name1,coeff1)::c,b1,(name1,coeff2 - coeff1)::b2)
107                          else ((name1,coeff2)::c,
108                                (name1,coeff1 - coeff2)::b1,
109                                b2)
110                      end)
111                  else if (name1 << name2) then
112                     (let val (c,b1,b2) =
113                             subtract_common_terms (tl bind1) bind2
114                      in  (c,(name1,coeff1)::b1,b2)
115                      end)
116                  else (let val (c,b1,b2) =
117                               subtract_common_terms bind1 (tl bind2)
118                        in  (c,b1,(name2,coeff2)::b2)
119                        end)
120             end
121 in fn tm =>
122 (let val (tm1,tm2) = dest_leq tm
123      val (const1,bind1) = coeffs_of_arith tm1
124      and (const2,bind2) = coeffs_of_arith tm2
125      val (bindc,bindl,bindr) = subtract_common_terms bind1 bind2
126      and (constc,constl,constr) =
127         if (const1 < const2)
128         then (const1, zero, const2 - const1)
129         else (const2, const1 - const2, zero)
130      val tml = build_arith (constl,bindl)
131      and tmr = build_arith (constr,bindr)
132  in  SYM
133       (((ADD_COEFFS_TO_LEQ_CONV (constc,bindc)) THENC
134         (ARGS_CONV (SORT_AND_GATHER_CONV THENC NORM_ZERO_AND_ONE_CONV)))
135        (mk_leq (tml,tmr)))
136  end
137 ) handle (HOL_ERR _) => failwith "LESS_OR_EQ_GATHER_CONV"
138 end;
139
140(*---------------------------------------------------------------------------*)
141(* ARITH_FORM_NORM_CONV : conv                                               *)
142(*                                                                           *)
143(* Converts an arithmetic formula into a disjunction of conjunctions of      *)
144(* less-than-or-equal-to inequalities. The arithmetic expressions are only   *)
145(* allowed to contain variables, addition, the SUC function, and             *)
146(* multiplication by constants. The formula is not allowed to contain        *)
147(* quantifiers, but may have disjunction, conjunction, negation,             *)
148(* implication, equality on Booleans, and the natural number relations       *)
149(* =, <, <=, >, >=.                                                          *)
150(*                                                                           *)
151(* The inequalities in the result are normalized so that each variable       *)
152(* appears on only one side of the inequality, and each side is a linear sum *)
153(* in which any constant appears first, followed by products of a constant   *)
154(* and a variable. The variables are ordered lexicographically, and if the   *)
155(* coefficient of the variable is 1, the product of 1 and the variable       *)
156(* appears in the term, not simply the variable.                             *)
157(*---------------------------------------------------------------------------*)
158
159fun ARITH_FORM_NORM_CONV tm =
160 (EQ_IMP_ELIM_CONV is_num_reln
161  THENC MOVE_NOT_DOWN_CONV is_num_reln
162          (NUM_RELN_NORM_CONV
163              (SUM_OF_PRODUCTS_CONV
164                 THENC LINEAR_SUM_CONV
165                 THENC SORT_AND_GATHER_CONV
166                 THENC NORM_ZERO_AND_ONE_CONV)
167              LESS_OR_EQ_GATHER_CONV)
168  THENC DISJ_NORM_FORM_CONV)
169 tm handle (HOL_ERR _) => failwith "ARITH_FORM_NORM_CONV";
170
171end
172