diff options
author | Tim King <taking@google.com> | 2017-01-04 12:57:55 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-01-04 12:57:55 -0800 |
commit | 4f8965352cacbc0cca9c88d71c1a69b7055822ef (patch) | |
tree | cc5f034ca0aed150937ab304c5837ed18d47fb12 /proofs/signatures/th_lra.plf | |
parent | a3094c713b73c6941f1f564bab33110927466526 (diff) |
Reverting two files encoding with DOS linebreaks back into using unix linebreaks.
Diffstat (limited to 'proofs/signatures/th_lra.plf')
-rw-r--r-- | proofs/signatures/th_lra.plf | 900 |
1 files changed, 449 insertions, 451 deletions
diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf index 88118e8d1..d67fdc84f 100644 --- a/proofs/signatures/th_lra.plf +++ b/proofs/signatures/th_lra.plf @@ -1,451 +1,449 @@ -; 59 loc in side conditions
-
-(program mpq_ifpos ((x mpq)) bool
- (mp_ifneg x ff (mp_ifzero x ff tt)))
-
-; a real variable
-(declare var_real type)
-; a real variable term
-(declare a_var_real (! v var_real (term Real)))
-
-;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n
-
-(declare lmon type)
-(declare lmonn lmon)
-(declare lmonc (! c mpq (! v var_real (! l lmon lmon))))
-
-(program lmon_neg ((l lmon)) lmon
- (match l
- (lmonn l)
- ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l')))))
-
-(program lmon_add ((l1 lmon) (l2 lmon)) lmon
- (match l1
- (lmonn l2)
- ((lmonc c' v' l')
- (match l2
- (lmonn l1)
- ((lmonc c'' v'' l'')
- (compare v' v''
- (lmonc c' v' (lmon_add l' l2))
- (lmonc c'' v'' (lmon_add l1 l''))))))))
-
-(program lmon_mul_c ((l lmon) (c mpq)) lmon
- (match l
- (lmonn l)
- ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c)))))
-
-;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c
-
-(declare poly type)
-(declare polyc (! c mpq (! l lmon poly)))
-
-(program poly_neg ((p poly)) poly
- (match p
- ((polyc m' p') (polyc (mp_neg m') (lmon_neg p')))))
-
-(program poly_add ((p1 poly) (p2 poly)) poly
- (match p1
- ((polyc c1 l1)
- (match p2
- ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2)))))))
-
-(program poly_sub ((p1 poly) (p2 poly)) poly
- (poly_add p1 (poly_neg p2)))
-
-(program poly_mul_c ((p poly) (c mpq)) poly
- (match p
- ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c)))))
-
-;; code to isolate a variable from a term
-;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t').
-
-(declare isol type)
-(declare isolc (! r mpq (! l lmon isol)))
-
-(program isolate_h ((v var_real) (l lmon) (e bool)) isol
- (match l
- (lmonn (isolc 0/1 l))
- ((lmonc c' v' l')
- (ifmarked v'
- (match (isolate_h v l' tt)
- ((isolc ci li) (isolc (mp_add c' ci) li)))
- (match e
- (tt (isolc 0/1 l))
- (ff (match (isolate_h v l' ff)
- ((isolc ci li) (isolc ci (lmonc c' v' li))))))))))
-
-(program isolate ((v var_real) (l lmon)) isol
- (do (markvar v)
- (let i (isolate_h v l ff)
- (do (markvar v) i))))
-
-;; determine if a monomial list is constant
-
-(program is_lmon_zero ((l lmon)) bool
- (match l
- (lmonn tt)
- ((lmonc c v l')
- (match (isolate v l)
- ((isolc ci li)
- (mp_ifzero ci (is_lmon_zero li) ff))))))
-
-;; return the constant that p is equal to. If p is not constant, fail.
-
-(program is_poly_const ((p poly)) mpq
- (match p
- ((polyc c' l')
- (match (is_lmon_zero l')
- (tt c')
- (ff (fail mpq))))))
-
-;; conversion to use polynomials in term formulas
-
-(declare poly_term (! p poly (term Real)))
-
-;; create new equality out of inequality
-
-(declare lra_>=_>=_to_=
- (! p1 poly
- (! p2 poly
- (! f1 (th_holds (>=0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds (=0_Real (poly_term p2))))))))))
-
-;; axioms
-
-(declare lra_axiom_=
- (th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))
-
-(declare lra_axiom_>
- (! c mpq
- (! i (^ (mpq_ifpos c) tt)
- (th_holds (>0_Real (poly_term (polyc c lmonn)))))))
-
-(declare lra_axiom_>=
- (! c mpq
- (! i (^ (mp_ifneg c tt ff) ff)
- (th_holds (>=0_Real (poly_term (polyc c lmonn)))))))
-
-(declare lra_axiom_distinct
- (! c mpq
- (! i (^ (mp_ifzero c tt ff) ff)
- (th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))
-
-;; contradiction rules
-
-(declare lra_contra_=
- (! p poly
- (! f (th_holds (=0_Real (poly_term p)))
- (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
- (holds cln)))))
-
-(declare lra_contra_>
- (! p poly
- (! f (th_holds (>0_Real (poly_term p)))
- (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
- (holds cln)))))
-
-(declare lra_contra_>=
- (! p poly
- (! f (th_holds (>=0_Real (poly_term p)))
- (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
- (holds cln)))))
-
-(declare lra_contra_distinct
- (! p poly
- (! f (th_holds (distinct0_Real (poly_term p)))
- (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)
- (holds cln)))))
-
-;; muliplication by a constant
-
-(declare lra_mul_c_=
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (=0_Real (poly_term p)))
- (! i (^ (poly_mul_c p c) p')
- (th_holds (=0_Real (poly_term p')))))))))
-
-(declare lra_mul_c_>
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (>0_Real (poly_term p)))
- (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
- (th_holds (>0_Real (poly_term p')))))))));)
-
-(declare lra_mul_c_>=
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (>=0_Real (poly_term p)))
- (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
- (th_holds (>=0_Real (poly_term p')))))))));)
-
-(declare lra_mul_c_distinct
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (distinct0_Real (poly_term p)))
- (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
- (th_holds (distinct0_Real (poly_term p')))))))));)
-
-;; adding equations
-
-(declare lra_add_=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (=0_Real (poly_term p3)))))))))))
-
-(declare lra_add_>_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_Real (poly_term p1)))
- (! f2 (th_holds (>0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_add_>=_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>=0_Real (poly_term p3))))))))))
-
-(declare lra_add_=_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (>0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_add_=_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>=0_Real (poly_term p3))))))))))
-
-(declare lra_add_>_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_Real (poly_term p1)))
- (! f2 (th_holds (>=0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_add_=_distinct
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (distinct0_Real (poly_term p2)))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (distinct0_Real (poly_term p3)))))))))))
-
-;; substracting equations
-
-(declare lra_sub_=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (=0_Real (poly_term p3)))))))))))
-
-(declare lra_sub_>_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (>0_Real (poly_term p3))))))))))
-
-(declare lra_sub_>=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (>=0_Real (poly_term p3))))))))))
-
-(declare lra_sub_distinct_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (distinct0_Real (poly_term p1)))
- (! f2 (th_holds (=0_Real (poly_term p2)))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (distinct0_Real (poly_term p3)))))))))))
-
- ;; converting between terms and polynomials
-
-(declare poly_norm (! t (term Real) (! p poly type)))
-
-(declare pn_let
- (! t (term Real)
- (! p poly
- (! pn (poly_norm t p)
-
- (! u (! pnt (poly_norm t p)
- (holds cln))
- (holds cln))))))
-
-(declare pn_const
- (! x mpq
- (poly_norm (a_real x) (polyc x lmonn))))
-
-(declare pn_var
- (! v var_real
- (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn)))))
-
-
-(declare pn_+
- (! x (term Real)
- (! px poly
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pnx (poly_norm x px)
- (! pny (poly_norm y py)
- (! a (^ (poly_add px py) pz)
- (poly_norm (+_Real x y) pz))))))))))
-
-(declare pn_-
- (! x (term Real)
- (! px poly
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pnx (poly_norm x px)
- (! pny (poly_norm y py)
- (! a (^ (poly_sub px py) pz)
- (poly_norm (-_Real x y) pz))))))))))
-
-(declare pn_mul_c_L
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py x) pz)
- (poly_norm (*_Real (a_real x) y) pz))))))))
-
-(declare pn_mul_c_R
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py x) pz)
- (poly_norm (*_Real y (a_real x)) pz))))))))
-
-;; for polynomializing other terms, in particular ite's
-
-(declare term_atom (! v var_real (! t (term Real) type)))
-
-(declare decl_term_atom
- (! t (term Real)
- (! u (! v var_real
- (! a (term_atom v t)
- (holds cln)))
- (holds cln))))
-
-(declare pn_var_atom
- (! v var_real
- (! t (term Real)
- (! a (term_atom v t)
- (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn)))))))
-
-
-;; conversion between term formulas and polynomial formulas
-
-(declare poly_formula_norm (! ft formula (! fp formula type)))
-
-; convert between term formulas and polynomial formulas
-
-(declare poly_form
- (! ft formula
- (! fp formula
- (! p (poly_formula_norm ft fp)
- (! u (th_holds ft)
- (th_holds fp))))))
-
-(declare poly_form_not
- (! ft formula
- (! fp formula
- (! p (poly_formula_norm ft fp)
- (! u (th_holds (not ft))
- (th_holds (not fp)))))))
-
-; form equivalence between term formula and polynomial formula
-
-(declare poly_norm_=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! h (th_holds (= Real x y))
- (! n (poly_norm (-_Real x y) p)
- (! u (! pn (th_holds (=0_Real (poly_term p)))
- (holds cln))
- (holds cln))))))))
-
-(declare poly_norm_>
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! h (th_holds (>_Real x y))
- (! n (poly_norm (-_Real x y) p)
- (! u (! pn (th_holds (>0_Real (poly_term p)))
- (holds cln))
- (holds cln))))))))
-
-(declare poly_norm_<
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! h (th_holds (<_Real x y))
- (! n (poly_norm (-_Real y x) p)
- (! u (! pn (th_holds (>0_Real (poly_term p)))
- (holds cln))
- (holds cln))))))))
-
-(declare poly_norm_>=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! h (th_holds (>=_Real x y))
- (! n (poly_norm (-_Real x y) p)
- (! u (! pn (th_holds (>=0_Real (poly_term p)))
- (holds cln))
- (holds cln))))))))
-
-(declare poly_norm_<=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! h (th_holds (<=_Real x y))
- (! n (poly_norm (-_Real y x) p)
- (! u (! pn (th_holds (>=0_Real (poly_term p)))
- (holds cln))
- (holds cln))))))))
-
-
+; 59 loc in side conditions + +(program mpq_ifpos ((x mpq)) bool + (mp_ifneg x ff (mp_ifzero x ff tt))) + +; a real variable +(declare var_real type) +; a real variable term +(declare a_var_real (! v var_real (term Real))) + +;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n + +(declare lmon type) +(declare lmonn lmon) +(declare lmonc (! c mpq (! v var_real (! l lmon lmon)))) + +(program lmon_neg ((l lmon)) lmon + (match l + (lmonn l) + ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l'))))) + +(program lmon_add ((l1 lmon) (l2 lmon)) lmon + (match l1 + (lmonn l2) + ((lmonc c' v' l') + (match l2 + (lmonn l1) + ((lmonc c'' v'' l'') + (compare v' v'' + (lmonc c' v' (lmon_add l' l2)) + (lmonc c'' v'' (lmon_add l1 l'')))))))) + +(program lmon_mul_c ((l lmon) (c mpq)) lmon + (match l + (lmonn l) + ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c))))) + +;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c + +(declare poly type) +(declare polyc (! c mpq (! l lmon poly))) + +(program poly_neg ((p poly)) poly + (match p + ((polyc m' p') (polyc (mp_neg m') (lmon_neg p'))))) + +(program poly_add ((p1 poly) (p2 poly)) poly + (match p1 + ((polyc c1 l1) + (match p2 + ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2))))))) + +(program poly_sub ((p1 poly) (p2 poly)) poly + (poly_add p1 (poly_neg p2))) + +(program poly_mul_c ((p poly) (c mpq)) poly + (match p + ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c))))) + +;; code to isolate a variable from a term +;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t'). + +(declare isol type) +(declare isolc (! r mpq (! l lmon isol))) + +(program isolate_h ((v var_real) (l lmon) (e bool)) isol + (match l + (lmonn (isolc 0/1 l)) + ((lmonc c' v' l') + (ifmarked v' + (match (isolate_h v l' tt) + ((isolc ci li) (isolc (mp_add c' ci) li))) + (match e + (tt (isolc 0/1 l)) + (ff (match (isolate_h v l' ff) + ((isolc ci li) (isolc ci (lmonc c' v' li)))))))))) + +(program isolate ((v var_real) (l lmon)) isol + (do (markvar v) + (let i (isolate_h v l ff) + (do (markvar v) i)))) + +;; determine if a monomial list is constant + +(program is_lmon_zero ((l lmon)) bool + (match l + (lmonn tt) + ((lmonc c v l') + (match (isolate v l) + ((isolc ci li) + (mp_ifzero ci (is_lmon_zero li) ff)))))) + +;; return the constant that p is equal to. If p is not constant, fail. + +(program is_poly_const ((p poly)) mpq + (match p + ((polyc c' l') + (match (is_lmon_zero l') + (tt c') + (ff (fail mpq)))))) + +;; conversion to use polynomials in term formulas + +(declare poly_term (! p poly (term Real))) + +;; create new equality out of inequality + +(declare lra_>=_>=_to_= + (! p1 poly + (! p2 poly + (! f1 (th_holds (>=0_Real (poly_term p1))) + (! f2 (th_holds (>=0_Real (poly_term p2))) + (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt) + (th_holds (=0_Real (poly_term p2)))))))))) + +;; axioms + +(declare lra_axiom_= + (th_holds (=0_Real (poly_term (polyc 0/1 lmonn))))) + +(declare lra_axiom_> + (! c mpq + (! i (^ (mpq_ifpos c) tt) + (th_holds (>0_Real (poly_term (polyc c lmonn))))))) + +(declare lra_axiom_>= + (! c mpq + (! i (^ (mp_ifneg c tt ff) ff) + (th_holds (>=0_Real (poly_term (polyc c lmonn))))))) + +(declare lra_axiom_distinct + (! c mpq + (! i (^ (mp_ifzero c tt ff) ff) + (th_holds (distinct0_Real (poly_term (polyc c lmonn))))))) + +;; contradiction rules + +(declare lra_contra_= + (! p poly + (! f (th_holds (=0_Real (poly_term p))) + (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff) + (holds cln))))) + +(declare lra_contra_> + (! p poly + (! f (th_holds (>0_Real (poly_term p))) + (! i2 (^ (mpq_ifpos (is_poly_const p)) ff) + (holds cln))))) + +(declare lra_contra_>= + (! p poly + (! f (th_holds (>=0_Real (poly_term p))) + (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt) + (holds cln))))) + +(declare lra_contra_distinct + (! p poly + (! f (th_holds (distinct0_Real (poly_term p))) + (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt) + (holds cln))))) + +;; muliplication by a constant + +(declare lra_mul_c_= + (! p poly + (! p' poly + (! c mpq + (! f (th_holds (=0_Real (poly_term p))) + (! i (^ (poly_mul_c p c) p') + (th_holds (=0_Real (poly_term p'))))))))) + +(declare lra_mul_c_> + (! p poly + (! p' poly + (! c mpq + (! f (th_holds (>0_Real (poly_term p))) + (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p') + (th_holds (>0_Real (poly_term p')))))))));) + +(declare lra_mul_c_>= + (! p poly + (! p' poly + (! c mpq + (! f (th_holds (>=0_Real (poly_term p))) + (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p') + (th_holds (>=0_Real (poly_term p')))))))));) + +(declare lra_mul_c_distinct + (! p poly + (! p' poly + (! c mpq + (! f (th_holds (distinct0_Real (poly_term p))) + (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p') + (th_holds (distinct0_Real (poly_term p')))))))));) + +;; adding equations + +(declare lra_add_=_= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (=0_Real (poly_term p1))) + (! f2 (th_holds (=0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (=0_Real (poly_term p3))))))))))) + +(declare lra_add_>_> + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (>0_Real (poly_term p1))) + (! f2 (th_holds (>0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (>0_Real (poly_term p3)))))))))) + +(declare lra_add_>=_>= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (>=0_Real (poly_term p1))) + (! f2 (th_holds (>=0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (>=0_Real (poly_term p3)))))))))) + +(declare lra_add_=_> + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (=0_Real (poly_term p1))) + (! f2 (th_holds (>0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (>0_Real (poly_term p3)))))))))) + +(declare lra_add_=_>= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (=0_Real (poly_term p1))) + (! f2 (th_holds (>=0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (>=0_Real (poly_term p3)))))))))) + +(declare lra_add_>_>= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (>0_Real (poly_term p1))) + (! f2 (th_holds (>=0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (>0_Real (poly_term p3)))))))))) + +(declare lra_add_=_distinct + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (=0_Real (poly_term p1))) + (! f2 (th_holds (distinct0_Real (poly_term p2))) + (! i (^ (poly_add p1 p2) p3) + (th_holds (distinct0_Real (poly_term p3))))))))))) + +;; substracting equations + +(declare lra_sub_=_= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (=0_Real (poly_term p1))) + (! f2 (th_holds (=0_Real (poly_term p2))) + (! i (^ (poly_sub p1 p2) p3) + (th_holds (=0_Real (poly_term p3))))))))))) + +(declare lra_sub_>_= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (>0_Real (poly_term p1))) + (! f2 (th_holds (=0_Real (poly_term p2))) + (! i (^ (poly_sub p1 p2) p3) + (th_holds (>0_Real (poly_term p3)))))))))) + +(declare lra_sub_>=_= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (>=0_Real (poly_term p1))) + (! f2 (th_holds (=0_Real (poly_term p2))) + (! i (^ (poly_sub p1 p2) p3) + (th_holds (>=0_Real (poly_term p3)))))))))) + +(declare lra_sub_distinct_= + (! p1 poly + (! p2 poly + (! p3 poly + (! f1 (th_holds (distinct0_Real (poly_term p1))) + (! f2 (th_holds (=0_Real (poly_term p2))) + (! i (^ (poly_sub p1 p2) p3) + (th_holds (distinct0_Real (poly_term p3))))))))))) + + ;; converting between terms and polynomials + +(declare poly_norm (! t (term Real) (! p poly type))) + +(declare pn_let + (! t (term Real) + (! p poly + (! pn (poly_norm t p) + + (! u (! pnt (poly_norm t p) + (holds cln)) + (holds cln)))))) + +(declare pn_const + (! x mpq + (poly_norm (a_real x) (polyc x lmonn)))) + +(declare pn_var + (! v var_real + (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn))))) + + +(declare pn_+ + (! x (term Real) + (! px poly + (! y (term Real) + (! py poly + (! pz poly + (! pnx (poly_norm x px) + (! pny (poly_norm y py) + (! a (^ (poly_add px py) pz) + (poly_norm (+_Real x y) pz)))))))))) + +(declare pn_- + (! x (term Real) + (! px poly + (! y (term Real) + (! py poly + (! pz poly + (! pnx (poly_norm x px) + (! pny (poly_norm y py) + (! a (^ (poly_sub px py) pz) + (poly_norm (-_Real x y) pz)))))))))) + +(declare pn_mul_c_L + (! y (term Real) + (! py poly + (! pz poly + (! x mpq + (! pny (poly_norm y py) + (! a (^ (poly_mul_c py x) pz) + (poly_norm (*_Real (a_real x) y) pz)))))))) + +(declare pn_mul_c_R + (! y (term Real) + (! py poly + (! pz poly + (! x mpq + (! pny (poly_norm y py) + (! a (^ (poly_mul_c py x) pz) + (poly_norm (*_Real y (a_real x)) pz)))))))) + +;; for polynomializing other terms, in particular ite's + +(declare term_atom (! v var_real (! t (term Real) type))) + +(declare decl_term_atom + (! t (term Real) + (! u (! v var_real + (! a (term_atom v t) + (holds cln))) + (holds cln)))) + +(declare pn_var_atom + (! v var_real + (! t (term Real) + (! a (term_atom v t) + (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn))))))) + + +;; conversion between term formulas and polynomial formulas + +(declare poly_formula_norm (! ft formula (! fp formula type))) + +; convert between term formulas and polynomial formulas + +(declare poly_form + (! ft formula + (! fp formula + (! p (poly_formula_norm ft fp) + (! u (th_holds ft) + (th_holds fp)))))) + +(declare poly_form_not + (! ft formula + (! fp formula + (! p (poly_formula_norm ft fp) + (! u (th_holds (not ft)) + (th_holds (not fp))))))) + +; form equivalence between term formula and polynomial formula + +(declare poly_norm_= + (! x (term Real) + (! y (term Real) + (! p poly + (! h (th_holds (= Real x y)) + (! n (poly_norm (-_Real x y) p) + (! u (! pn (th_holds (=0_Real (poly_term p))) + (holds cln)) + (holds cln)))))))) + +(declare poly_norm_> + (! x (term Real) + (! y (term Real) + (! p poly + (! h (th_holds (>_Real x y)) + (! n (poly_norm (-_Real x y) p) + (! u (! pn (th_holds (>0_Real (poly_term p))) + (holds cln)) + (holds cln)))))))) + +(declare poly_norm_< + (! x (term Real) + (! y (term Real) + (! p poly + (! h (th_holds (<_Real x y)) + (! n (poly_norm (-_Real y x) p) + (! u (! pn (th_holds (>0_Real (poly_term p))) + (holds cln)) + (holds cln)))))))) + +(declare poly_norm_>= + (! x (term Real) + (! y (term Real) + (! p poly + (! h (th_holds (>=_Real x y)) + (! n (poly_norm (-_Real x y) p) + (! u (! pn (th_holds (>=0_Real (poly_term p))) + (holds cln)) + (holds cln)))))))) + +(declare poly_norm_<= + (! x (term Real) + (! y (term Real) + (! p poly + (! h (th_holds (<=_Real x y)) + (! n (poly_norm (-_Real y x) p) + (! u (! pn (th_holds (>=0_Real (poly_term p))) + (holds cln)) + (holds cln)))))))) |