Source File | Identifier index | Theory binding index |
---|

signature OmegaMath = sig include Abbrev val find_summand : term -> term -> term val gcd_eq_check : conv val gcd_le_check : conv val gcd_check : conv val addzero : conv val SORT_AND_GATHER1_CONV : conv val SORT_AND_GATHER_CONV : conv val S_AND_G_MULT : conv val MOVE_VCOEFF_TO_FRONT : term -> conv val NEG_SUM_CONV : conv val NORMALISE_MULT : conv val leaf_normalise : conv val sum_normalise : conv val PRENEX_CONV : conv val cond_removal : conv val eliminate_positive_divides : conv val eliminate_negative_divides : conv val calculate_range_disjunct : conv val OmegaEq : conv end (* [find_summandv tm] finds the summand involving variable v in tm. Raise a HOL_ERR if it's not there. tm must be a left-associated sum with one numeral in the rightmost position. [gcd_eq_checktm] returns a theorem equating tm to an improved equivalent, or QConv.UNCHANGED, if no improvement is possible. tm must be of the form 0 = r1 + .. + rn where rn is a numeral and all of the other ri's are of the form (numeral * variable) If all of the variables have coefficients divisible by some common factor, then this conversion returns an equality either with all the coefficients appropriately smaller, or equating it to false (which will happen if there the numeral term is of the wrong divisibility). [gcd_le_checktm] returns a theorem equating tm to an improved equivalent (as per gcd_eq_check), or QConv.UNCHANGED, if no improvement is possible. tm must be of the form 0 <= (c1 * v1) + (c2 * v2) + .. + (cn * vn) + n [gcd_checktm] applies either gcd_eq_check or gcd_le_check depending on tm's relational operator. Fails with HOL_ERR otherwise. [addzerot] if t (of integer type and not a numeral itself) does not have a numeral as its 'rand, then return thm |- t = t + 0, otherwise ALL_CONV. [SORT_AND_GATHER1_CONVtm] performs one step of an "insertion sort"; modifying a term of the form x + y, with x a normalised sum, and y a singleton summand, so that y is inserted into x, merging with any appropriate other summands, and possibly cancelling others out. [SORT_AND_GATHER_CONVtm] performs all the steps of the insertion sort, collecting up variable coefficients and producing a left associated term with variables appearing in sorted order. [S_AND_G_MULTtm] performs a sort-and-gather step, and also copes with distributing multiplications over sub-summands, as long as the constant to be multiplied through is on the left side of the multiplication. [MOVE_VCOEFF_TO_FRONTv tm] turns c1 * v1 + ... + c * v + ... cn * vn + n into c * v + (c1 * v1 + ... + cn * vn + n) [NEG_SUM_CONV] simplifies ~(c1*v1 + c2 * v2 .. + cn * vn + n), by pushing the negation inwards. [NORMALISE_MULTtm] normalises the multiplicative term tm, gathering up coefficients, and turning it into the form n * (v1 * v2 * ... vn), where n is a numeral and the v's are the variables in the term, sorted into the order specified by Term.compare. Works over both :num and :int. [leaf_normaliset] normalises a "leaf term" t (a relational operator over integer values) to either an equality, a <= or a disjunction of two normalised <= leaves. (The latter happens if called onto normalise ~(x = y)). [sum_normaliset] normalises a term of type :int into the standard Omega normal form, where the resulting term is of the form c1 * v1 + c2 * v2 + c3 * v3 + ... + cn * vn + c where the c is always present and maybe 0. [PRENEX_CONVt] normalises t by pulling quantifiers to the front, over boolean connectives such as ~ /\ \/ and also if-then-else, as long as the quantifier is not in the guard of the latter. [cond_removalt] removes those conditional expressions from t that repeat their guards, and introduces a case split (i.e., disjunctions) at the top level of the term to reflect this. Don't use if you want to generate CNF. [eliminate_positive_dividest] where t is a term of the form ?x1 .. xn. body where body is a conjunction of leaves, possibly including divisibility relations (negated or positive). This function writes away those (positive) divisibility relations of the form d | exp where exp includes at least one variable from x1 .. xn. [eliminate_negative_dividest] where t is a term of the form ?x1 .. xn. body where body is a conjunction of leaves, possibly including divisibility relations (negated or positive). This function writes away those negated divisibility relations of the form ~(d | exp) where exp includes at least one variable from x1 .. xn. It introduces case splits in the body (at least where d is not 2), and pushes the existential variables over the resulting disjunctions. It doesn't eliminate the positive divisibility terms that result. [calculate_range_disjunctt] where t is of the form ?i. (lo <= i /\ i <= hi) /\ ... and lo and hi are integer literal. Transforms this into an appropriate number of disjuncts (or possibly false, if hi < lo, of the form P(lo) \/ P (lo + 1) \/ .. P (hi) but where the additions (lo + 1 etc) are reduced to literals [OmegaEqt] simplifies an existentially quantified Presburger term, (or returns QConv.UNCHANGED) by using the equality elimination procedure described in section 2.2 of Pugh's CACM paper. The term t should be of the form ?v1..vn. body If the conversion is to do anything other than return UNCHANGED, there should be a Omega-normalised equality in (strip_conj body). *)

Source File | Identifier index | Theory binding index |
---|