Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/Sturm/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 7.10.2014 mit Größe 5 kB

Quelle sturmsquarefree.pvs Sprache: PVS

sturmsquarefree: THEORY
BEGIN

IMPORTING reals@polynomials,reals@more_polynomial_props,reals@sign,
   polynomial_division,
          number_sign_changes,
          structures@more_list_props,ints@gcd,
   gcd_coeff,structures@sort_array

  a,r : VAR [nat->real]
  p : VAR [nat->[nat->real]]
  n : VAR [nat->nat]
  d,m,i,j,k : VAR nat
  x,y,c,b : VAR real

  sturm_sequence?(p,n,m): bool =
    LET P = (LAMBDA (k): polynomial(p(k),n(k))) IN
      (FORALL (i): i<m IMPLIES (n(i)>n(i+1) OR n(i+1)=0))  % Decreasing Degree
      AND (FORALL (i): i<=m IMPLIES p(i)(n(i))/=0)
      AND (FORALL (x): P(0)(x)=0
             IMPLIES sign_ext(P(1)(x)) =
        sign_ext(polynomial(poly_deriv(p(0)),max(n(0)-1,0))(x)))
      AND (FORALL (x,i): 0<i AND i<m AND P(i)(x)=0 IMPLIES
         sign_ext(P(i-1)(x)) = -sign_ext(P(i+1)(x)))
      AND (FORALL (x,y): sign_ext(P(m)(x)) = sign_ext(P(m)(y)))

  sturm_sequence_degree_1: LEMMA
    n(0)=1 AND n(1)=0 AND p(0)(1)/=0 AND p(1) = poly_deriv(p(0))
    IMPLIES
    sturm_sequence?(p,n,1)

  sturm_seq_repeated_root: LEMMA sturm_sequence?(p,n,m) IMPLIES
    FORALL (i:nat): i+1<=m AND
    polynomial(p(i),n(i))(x)=0 AND polynomial(p(i+1),n(i+1))(x)=0
    IMPLIES
    (FORALL (j:upto(m)): polynomial(p(j),n(j))(x) = 0)

  sturm_seq_last_nonzero: LEMMA
    m>0 AND
    sturm_sequence?(p,n,m) AND
    (FORALL (c:real): polynomial(p(0),n(0))(c)=0 IMPLIES
      polynomial(p(1),n(1))(c)/=0)
    IMPLIES
    FORALL (xyz:real): polynomial(p(m),n(m))(xyz)/=0

  sturm_sig(p,n,m)(x): nat = number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(x),m)`num

  % Part 1: Proving Sturm's Theorem when f has no multiple roots

  sturm_seq_first_signs_eq: LEMMA
    x<b AND b<y AND
    polynomial(p(0),n(0))(b)=0 AND
    (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIES
      (polynomial(p(1),n(1))(c)/=0 AND c = b)) AND
    sturm_sequence?(p,n,m)
    IMPLIES
    (polynomial(p(0),n(0))(x)/=0 AND
     polynomial(p(0),n(0))(y)/=0 AND
     sign_ext(polynomial(p(0),n(0))(x)) = -sign_ext(polynomial(p(1),n(1))(b)) AND
     sign_ext(polynomial(p(0),n(0))(y)) = sign_ext(polynomial(p(1),n(1))(b)))

  sturm_lem_no_roots: LEMMA
    x<y AND
    (FORALL (c:real,i:nat): i<=m AND x<=c AND c<=y IMPLIES polynomial(p(i),n(i))(c)/=0) AND
    sturm_sequence?(p,n,m)
    IMPLIES
    sturm_sig(p,n,m)(x) = sturm_sig(p,n,m)(y)

  sturm_lem_one_root: LEMMA
    x<y AND x<b AND b<y AND
    (FORALL (c:real,i:nat): i<=m AND x<=c AND c<=y AND polynomial(p(i),n(i))(c)=0
     IMPLIES c = b) AND
    (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIES
      (polynomial(p(1),n(1))(c)/=0))
    AND j<=m AND polynomial(p(j),n(j))(b)/=0 AND
    sturm_sequence?(p,n,m)
    IMPLIES
    LET nsc = LAMBDA (xyz:real,pj:nat): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),pj) IN
      sign_ext(nsc(x,j)`lastnz) = sign_ext(nsc(y,j)`lastnz) AND
      nsc(x,j)`num = nsc(y,j)`num+(IF polynomial(p(0),n(0))(b)=0 THEN 1 ELSE 0 ENDIF)

  sturm_lem_edge_root: LEMMA
    x<y AND
    (FORALL (c:real,i:nat): i<=m AND x<=c AND c<=y AND polynomial(p(i),n(i))(c)=0
     IMPLIES c = y) AND
    (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIES
      (polynomial(p(1),n(1))(c)/=0))
    AND j<=m AND polynomial(p(j),n(j))(y)/=0 AND
    sturm_sequence?(p,n,m) AND
    p(1) = poly_deriv(p(0)) AND n(1) = n(0)-1
    IMPLIES
    LET nsc = LAMBDA (xyz:real,pj:nat): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),pj) IN
      sign_ext(nsc(x,j)`lastnz) = sign_ext(nsc(y,j)`lastnz) AND
      nsc(x,j)`num = nsc(y,j)`num+(IF polynomial(p(0),n(0))(y)=0 THEN 1 ELSE 0 ENDIF)

  roots_between_enum: LEMMA % THIS NEEDS TO BE FOR ALL P(i) NOT JUST P(0)
    x<y AND sturm_sequence?(p,n,m) IMPLIES
      EXISTS ((K:nat|K>=2),enum:[below(K)->real]):
        (FORALL (i,j:below(K)): i<j IMPLIES enum(i)<enum(j)) AND
   enum(0)=x AND enum(K-1)=y AND
   (FORALL (b:real,j:nat): j<=m AND x<b AND b<=y AND polynomial(p(j),n(j))(b)=0 IMPLIES
     EXISTS (i:below(K)): b = enum(i))

  sturm_lem_no_roots_full: LEMMA
    m>0 AND x<y AND
    (FORALL (c:real,i:nat): i<=m AND x<c AND c<=y IMPLIES polynomial(p(i),n(i))(c)/=0) AND
    sturm_sequence?(p,n,m) AND
    (FORALL (c:real): polynomial(p(0),n(0))(c)=0 IMPLIES
      polynomial(p(1),n(1))(c)/=0) AND
    p(1) = poly_deriv(p(0)) AND n(1) = n(0)-1
    IMPLIES
    sturm_sig(p,n,m)(x) = sturm_sig(p,n,m)(y)

  sturm_square_free: LEMMA
    m>0 AND x<y AND (EXISTS (i:upto(n(0))): p(0)(i)/=0) AND
    (FORALL (c:real): polynomial(p(0),n(0))(c)=0 IMPLIES
      (polynomial(p(1),n(1))(c)/=0)) AND
    sturm_sequence?(p,n,m) AND
    p(1) = poly_deriv(p(0)) AND n(1) = n(0)-1
    IMPLIES
      LET nsc = LAMBDA (xyz:real): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),m),
         Nroots = nsc(x)`num-nsc(y)`num
      IN Nroots>=0 AND EXISTS (bij: [below(Nroots)->{xr:real|x<xr AND xr<=y AND polynomial(p(0),n(0))(xr)=0}]):
           bijective?(bij)

  sturm_seq_square_free: LEMMA
    (m>0 AND n(m)=0 AND (FORALL (i:below(m)): p(i)(n(i))/=0) AND
    (FORALL (i,j:upto(m)): i<j IMPLIES n(i)>n(j)) AND
    (FORALL (c:real): polynomial(p(0),n(0))(c)=0 IMPLIES
      (polynomial(p(1),n(1))(c)/=0)) AND
    p(1) = poly_deriv(p(0)) AND n(1) = n(0)-1 AND
    (FORALL (j:nat): j>1 AND j<=m IMPLIES LET pd = poly_divide(p(j-2),n(j-2))(p(j-1),n(j-1))(0) IN
                        EXISTS (c:posreal):
                        polynomial(p(j),n(j)) =
        polynomial(-c*pd`rem,pd`rdeg)))
    IMPLIES
      (p(m)(0)/=0 AND sturm_sequence?(p,n,m)) OR
      (p(m)(0) =0 AND sturm_sequence?(p,n,m-1))

END sturmsquarefree

quality68%

¤ 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.