|
poly_system_strategy: THEORY
BEGIN
% Systems of Polynomials
IMPORTING poly_systems,system_solvers
a,r,g : VAR [nat->int]
p : VAR [nat->[nat->int]]
relseq: VAR [nat->RealOrder]
n : VAR [nat->nat]
d,i,j,k : VAR nat
m: VAR posnat
%m : VAR posnat
x,y,c,b : VAR real
babove,bbelow,bbelow2,babove2: VAR bool
RelF6,TQRow: VAR [nat->subrange(0,5)]
% Next is a function that takes a system, possibly involving only inequalities and not equalities,
% and converts it to a system(s) with at least one equality.
strictify(RelF6)(i): subrange(0,5) = IF RelF6(i)=4 THEN 1 ELSIF RelF6(i)=5 THEN 2 ELSE RelF6(i) ENDIF
first_eq(RelF6,k): RECURSIVE {i | (i>k IMPLIES FORALL (j:upto(k)): RelF6(j)>0) AND
(i<=k IMPLIES RelF6(i)=0 AND FORALL (j): j<i IMPLIES RelF6(j)>0)} =
IF k=0 THEN (IF RelF6(0)=0 THEN 0 ELSE 1 ENDIF)
ELSE LET last = first_eq(RelF6,k-1) IN
IF last>k-1 THEN (IF RelF6(k)=0 THEN k ELSE k+1 ENDIF)
ELSE last ENDIF
ENDIF MEASURE k
prod_nonstrict(k,p,(n|FORALL (j:upto(k)): p(j)(n(j))/=0),RelF6): list[int] =
prod_polynomials_list(LAMBDA (i): IF RelF6(i)>=4 THEN p(i) ELSE (LAMBDA (j:nat): 1) ENDIF,
LAMBDA (i): IF RelF6(i)>=4 THEN n(i) ELSE 0 ENDIF,(LAMBDA (i): 1),k)
rel5(i:subrange(0,5))(r1,r2:real): bool =
(IF i=0 THEN r1=r2 ELSIF i=1 THEN r1>r2
ELSIF i=2 THEN r1<r2 ELSIF i=3 THEN r1/=r2
ELSIF i=4 THEN r1>=r2 ELSIF i=5 THEN r1<=r2 ELSE TRUE ENDIF)
solvable_at?(k,p,(n|FORALL (j:upto(k)): p(j)(n(j))/=0),RelF6)(x): bool =
FORALL (i:upto(k)):
rel5(RelF6(i))(polynomial(p(i),n(i))(x),0)
solvable?(k,p,(n|FORALL (j:upto(k)): p(j)(n(j))/=0),RelF6): bool =
EXISTS (x): solvable_at?(k,p,n,RelF6)(x)
greatify_poly(i:subrange(0,5),a): [nat->int] =
IF i=2 OR i=5 THEN (-1)*a ELSE a ENDIF
greatify_poly_rel(p,RelF6)(i): [nat->int] =
greatify_poly(RelF6(i),p(i))
greatify_rel(RelF6)(i): {pz:subrange(0,5)|pz/=2 AND pz/=5} =
IF RelF6(i)=2 THEN 1 ELSIF RelF6(i)=5 THEN 4 ELSE RelF6(i) ENDIF
greatify_def: LEMMA (FORALL (j:upto(k)): p(j)(n(j))/=0) IMPLIES
(solvable?(k,p,n,RelF6) IFF
solvable?(k,greatify_poly_rel(p,RelF6),n,greatify_rel(RelF6)))
compute_solvable_single(i:subrange(0,5),a,(d|a(d)/=0)): bool =
IF d=0 THEN rel5(i)(a(0),0)
ELSIF d=1 THEN TRUE
ELSIF i=3 THEN TRUE
ELSE LET iseq = sturm_tarski_faster(1,a,d,LAMBDA (k):LAMBDA (j):1,
LAMBDA (k):0,LAMBDA (j):1)/=0
IN IF i=0 THEN iseq
ELSIF i/=1 AND i/=2 AND iseq THEN TRUE
ELSE LET newa = IF rel5(i)(1,0) THEN a ELSE (-1)*a ENDIF
IN
newa(d)>0 OR (odd?(d) AND newa(d)<0) OR
sturm_tarski_faster(1,poly_deriv(a),d-1,LAMBDA (j): newa,
LAMBDA (j): d,greatify_rel(LAMBDA (j): i))/=0
ENDIF
ENDIF
compute_solvable_single_def: LEMMA a(d)/=0 IMPLIES FORALL (i:subrange(0,5)):
(EXISTS (x): rel5(i)(polynomial(a,d)(x),0)) IFF
compute_solvable_single(i,a,d)
poly_deriv_integer: LEMMA
rational_pred(poly_deriv(a)(d)) AND
integer_pred(poly_deriv(a)(d))
compute_solvable(k,p,(n|FORALL (j:upto(k)): p(j)(n(j))/=0 AND n(j)>0),RelF6): bool =
LET newp=greatify_poly_rel(p,RelF6),
newRel=greatify_rel(RelF6)
IN
IF k=0 THEN compute_solvable_single(RelF6(0),p(0),n(0))
ELSIF (EXISTS (i:upto(k)): newRel(i)=0) THEN
LET fe = first_eq(newRel,k) IN
sturm_tarski_faster(k-1,newp(fe),n(fe),
(LAMBDA (i): IF i<fe THEN newp(i) ELSE newp(i+1) ENDIF),
(LAMBDA (i): IF i<fe THEN n(i) ELSE n(i+1) ENDIF),
(LAMBDA (i): IF i<fe THEN newRel(i) ELSE newRel(i+1) ENDIF))/=0
ELSE
LET Qprodlist = prod_polynomials_list(newp,n,LAMBDA i: 1,k),
Qdeg = length(Qprodlist)-1,
Qprod = (LAMBDA (i): IF i<length(Qprodlist) THEN nth(Qprodlist,i) ELSE 0 ENDIF)
IN
(Qdeg>0 AND sturm_tarski_faster(k,Qprod,Qdeg,newp,n,newRel)/=0)
OR
(Qdeg>=2 AND
((FORALL (j:upto(k)): rel5(newRel(j))(newp(j)(n(j)),0)) OR
(FORALL (j:upto(k)): (odd?(n(j)) IMPLIES rel5(newRel(j))(-newp(j)(n(j)),0)) AND
(even?(n(j)) IMPLIES rel5(newRel(j))(newp(j)(n(j)),0))) OR
sturm_tarski_faster(k,poly_deriv(Qprod),Qdeg-1,newp,n,newRel)/=0))
ENDIF
compute_solvable_def: LEMMA
(FORALL (j:upto(k)): p(j)(n(j))/=0 AND n(j)>0) IMPLIES
((EXISTS (x:real): FORALL (j:upto(k)): rel5(RelF6(j))(polynomial(p(j),n(j))(x),0)) IFF
compute_solvable(k,p,n,RelF6))
poly_system_list(k,p,(n|FORALL (j:upto(k)): p(j)(n(j))/=0 AND n(j)>0)): {lli : list[list[int]] |
length[list[int]](lli) = k+1 AND (FORALL (i:upto(k)): length[int](nth[list[int]](lli,i)) = n(i)+1) AND
(FORALL (j:upto(k),i:upto(n(j))): nth[int](nth[list[int]](lli,j),i)=p(j)(i))} =
array2list[list[int]](k+1)(LAMBDA (j:nat): array2list[int](n(j)+1)(p(j)))
pq: VAR [nat->[nat->rat]]
tarski(k,pq,(n|FORALL (j:upto(k)): pq(j)(n(j))/=0 AND n(j)>0),RelF6): bool =
LET pi = (LAMBDA (j): rat_poly_to_int(pq(j),n(j))),
pl = poly_system_list(k,pi,n),
p = (LAMBDA (i): LAMBDA (j): IF i<=k AND j<=n(i) THEN nth[int](nth[list[int]](pl,i),j) ELSE 0 ENDIF)
IN compute_solvable(k,p,n,RelF6)
tarski_def: LEMMA
(FORALL (j:upto(k)): pq(j)(n(j))/=0 AND n(j)>0) IMPLIES
((EXISTS (x:real): FORALL (j:upto(k)): rel5(RelF6(j))(polynomial(pq(j),n(j))(x),0)) IFF
tarski(k,pq,n,RelF6))
END poly_system_strategy
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
