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