SSL poly_system_strategy.pvs Sprache: PVS

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

quality64%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.