# Structure OmegaSimple

signature OmegaSimple =
sig
include Abbrev
val simple_CONV : conv
val verify_result : term -> term list -> term OmegaMLShadow.result -> thm
val verify_satisfaction : term -> term list -> Arbint.int PIntMap.t -> thm
val verify_derivation :
term -> term list -> term OmegaMLShadow.derivation -> thm
val verify_contr : (thm * thm) -> thm
val verify_gcd_check : thm -> thm
val verify_combination : term -> thm -> thm -> thm
end
(*
This file turns the "external proofs" returned by the OmegaMLShadow
implementation into HOL kernel proofs. It also performs the initial
translation from a HOL formula into a shadow proof state, so that the
simple_CONV function can do an entire proof.
[**simple_CONV** t] tries to prove t using the OmegaMLShadow approach. The
input term must be of the form
?x1..xn. body
with body being a conjunction of terms, all of the form
0 <= c1 * v1 + .. cn * vn + c
with v1 < v2 < .. < vn according to the standard Term ordering. (The
ordering of x1..xn in the existential quantification isn't important.)
The final term constant c must always be present, even if it is zero.
[**verify_result** tm vars r] takes a term and a result from the
MLShadow and attempts to turn it into a theorem, where vars is the
list of variables occuring in tm, in order.
[**verify_satisfaction** tm vars vm] proves formula tm true by providing
witnesses for the variables. vm maps indices from the list of vars
to the values that those variables should take on.
[**verify_derivation** tm vars d] takes a purported derivation of
false from the assumption tm, and uses it to equate tm to false.
vars is the list of variables in tm, in order.
[**verify_contr** (th1, th2)] returns [..] |- F, given the theorems th1
and th2, which between them say contradictory things. They will
be of the form 0 <= X + c and 0 <= ~X + d and ~c is not <= d. X
may be the sum of multiple ci * vi pairs.
[**verify_gcd_check** th] eliminates a common divisor from the
coefficients of the variables in theorem th, which is of the
standard form.
[**verify_combination** v th1 th2] does variable elimination on v,
given a "lower-bound" theorem th1, and an "upper-bound" theorem
th2. Both th1 and th2 are of the form
0 <= c1 * v1 + ... + vn * cn + n
In th1, the coefficient of v will be positive, and in th2,
negative.
*)

*HOL 4, Kananaskis-13*