Quelle  poly_system_strategy.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