SSL poly_systems.pvs

poly_systems: THEORY
BEGIN

% Systems of Polynomials 

IMPORTING reals@polynomials,reals@more_polynomial_props,reals@sign,reals@real_orders,
   structures@sort_array,tarski_query_matrix

  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)]

  system_roots_enum: LEMMA 
    (FORALL (i):i<=k IMPLIES p(i)(n(i))/=0) IMPLIES
      EXISTS (K:nat,enum:[below(K)->real]):
        (FORALL (i,j:below(K)): i<j IMPLIES enum(i)<enum(j)) AND
 (FORALL (i:below(K)): EXISTS (j): j<=k AND polynomial(p(j),n(j))(enum(i))=0) AND
   (FORALL (b,j): j<=k AND polynomial(p(j),n(j))(b)=0 IMPLIES
     EXISTS (i:below(K)): b = enum(i))

  strict_poly_system_solvable: LEMMA (FORALL (i):i<=k IMPLIES p(i)(n(i))/=0) IMPLIES
    ((EXISTS (x): FORALL (i): i<=k IMPLIES polynomial(p(i),n(i))(x)>0)
    IFF
    ((FORALL (i): i<=k IMPLIES p(i)(n(i))>0) OR
     (FORALL (i): i<=k IMPLIES (IF odd?(n(i)) THEN -1 ELSE 1 ENDIF)*p(i)(n(i))>0) OR
     (EXISTS (x): (LET Q = prod_polynomials(p,n,(LAMBDA (i:nat): 1),k),Qdeg = sigma(0,k,n) IN
         Qdeg>0 AND polynomial(poly_deriv(Q),Qdeg-1)(x)=0) AND FORALL (i): i<=k 
      IMPLIES polynomial(p(i),n(i))(x)>0)))

  % The following function computes the number of solutions to poly(a,m)(x)=0 
  % AND poly(p(i),n(i))(x)>0 for i<=k. Another version will be formed below.


  A63_tensor_power_mat_row(m)(RelF6): RECURSIVE {M:PosFullMatrix|rows(M)=1 AND columns(M)=3^m} =
    IF m = 1 THEN vect2matrix(row(A63)(RelF6(0)))
    ELSE tensor_prod(A63_tensor_power_mat_row(m-1)((LAMBDA (d): RelF6(d+1))),
            vect2matrix(row(A63)(RelF6(0))))
    ENDIF MEASURE m

  A63_tensor_power_mat_row_def: LEMMA 
    LET ii = base_n_to_nat(6,RelF6,k) IN
      A63_tensor_power_mat_row(1+k)(RelF6) =
      vect2matrix(row(tensor_power_alt(A63,1+k))(ii))

  sturm_tarski_solver_slow_basic(k,a,(m|a(m)/=0),p,
                (n|FORALL (i:upto(k)):p(i)(n(i))/=0),RelF6):
    {r:real | r = NSol_all(k,a,m,p,n,RelF6) AND rational_pred(r) AND integer_pred(r)} =
        super_dot(row(A63_tensor_power_mat_row(k+1)(RelF6))(0),col(TQ_vect3k(k,a,m,p,n))(0))





END poly_systems