Quelle  tarski_query.pvs   Sprache: PVS

tarski_query: THEORY
BEGIN


IMPORTING poly_families, reals@product_nat,
          matrices@tensor_product, matrices@matrices,
   matrices@query_coeff

  a,r,g : VAR [nat->int]
  n : VAR posnat
  d,i,j,k : VAR nat
  m: VAR posnat
  x,y,c,b : VAR real
  rel: VAR [[real,real]->bool]
  babove,bbelow,bbelow2,babove2: VAR bool

  % k is the degree of g

  NSol_squared_gt: LEMMA a(n)/=0 IMPLIES
    NSol(a,n,polynomial_prod(g,k,g,k),2*k,>) =
    NSol(a,n,g,k,/=)

  NSol_squared_lt: LEMMA a(n)/=0 IMPLIES
    NSol(a,n,polynomial_prod(g,k,g,k),2*k,<) = 0

  NSol_poly1_lt: LEMMA a(n)/=0 IMPLIES
    NSol(a,n,poly1,0,<)=0

  A3: {M: PosFullMatrix | rows(M)=3 AND columns(M)=3} =
    (: (: 1, 0, -1 :), (: 0, 1/2, 1/2 :), (: 0, -1/2, 1/2 :) :)

  A3_inv: {M: PosFullMatrix | rows(M)=3 AND columns(M)=3 AND det(M)/=0 AND inverse(M)=A3} =
    (: (: 1,1,1 :), (: 0,1,-1 :), (: 0,1,1 :) :)

  TQ_vect3(a,(n|a(n)/=0),g,(k|g(k)/=0)): {v: PosFullMatrix | rows(v)=3 AND columns(v)=1} =
    (: (: TQ(a,n,poly1,0) :),(: TQ(a,n,g,k) :), (: TQ(a,n,polynomial_prod(g,k,g,k),2*k) :) :)

  NSol_vect3(a,(n|a(n)/=0),g,(k|g(k)/=0)): {v: PosFullMatrix | rows(v)=3 AND columns(v)=1} =
    (: (: NSol(a,n,g,k,=) :),(: NSol(a,n,g,k,>) :), (: NSol(a,n,g,k,<) :) :)

  tarski_query_system_basic_3: LEMMA a(n)/=0 AND g(k)/=0 IMPLIES
    A3*TQ_vect3(a,n,g,k) = NSol_vect3(a,n,g,k)

  A6: {M: PosFullMatrix | rows(M)=6 AND columns(M)=3} =
    (: (: 1, 0, -1 :), 
       (: 0, 1/2, 1/2 :), 
       (: 0, -1/2, 1/2 :),
       (: 0,0,1 :), 
       (: 1,1/2,-1/2 :), 
       (: 1,-1/2,-1/2 :) :)

  NSol_vect6(a,(n|a(n)/=0),g,(k|g(k)/=0)): {v: PosFullMatrix | rows(v)=6 AND columns(v)=1} =
    (: (: NSol(a,n,g,k,=) :),(: NSol(a,n,g,k,>) :), (: NSol(a,n,g,k,<) :),
       (: NSol(a,n,g,k,/=) :),(: NSol(a,n,g,k,>=) :), (: NSol(a,n,g,k,<=) :) :)

  tarski_query_system_basic_6: LEMMA a(n)/=0 AND g(k)/=0 IMPLIES
    A6*TQ_vect3(a,n,g,k) = NSol_vect6(a,n,g,k)

END tarski_query