Quelle clear_denominators.pvs Sprache: PVS

clear_denominators: THEORY
BEGIN

  IMPORTING ints@gcd

x,y : VAR posrat
i   : VAR int
n   : VAR nat
pn  : VAR posnat

PosRatPair: TYPE = [# num:posnat,den:posnat #]

prp,prp1,prp2: VAR PosRatPair

posratpair_convert(prp): posrat = prp`num/prp`den;

+(prp1,prp2):PosRatPair = (# num:=prp1`num*prp2`den+prp2`num*prp1`den,
        den:=prp1`den*prp2`den #);

posratpair_plus: LEMMA posratpair_convert(prp1)+posratpair_convert(prp2)=
         posratpair_convert(prp1+prp2);

/(prp1,prp2):PosRatPair = (# num:=prp1`num*prp2`den,
        den:=prp1`den*prp2`num #);

posratpair_div: LEMMA posratpair_convert(prp1)/posratpair_convert(prp2)=
         posratpair_convert(prp1/prp2);

PosRatSet(x): set[posnat]= {N:posnat | EXISTS (pn1,pn2:posnat):
             x=pn1/pn2 AND N=pn1+pn2}

PosRatSet_nonempty: LEMMA nonempty?(PosRatSet(x))

PosRatSet_glb_posnat: LEMMA EXISTS (pn:posnat):
  PosRatSet(x)(pn) AND
  pn = glb(PosRatSet(x))

PosRatMeas(x): nat =
  LET mp:posnat = glb(PosRatSet(x)) IN
    IF x<1 THEN 10^mp ELSE 10^mp - 1 ENDIF

PosRatMeas_increasing: LEMMA
  (EXISTS (pn:(PosRatSet(x))): FORALL (pm:(PosRatSet(y))): pn<pm)
  IMPLIES PosRatMeas(x)<PosRatMeas(y)

PosRatMeas_glb_minus_posnat: LEMMA x>pn IMPLIES
  glb(PosRatSet(x-pn)) <= glb(PosRatSet(x))-pn

compute_posratpair(x:posrat): RECURSIVE {prp | posratpair_convert(prp)=x} =
  IF floor(x)=x THEN (# num:=floor(x),den:=1 #)
  ELSIF x>1 THEN (# num:=floor(x),den:=1 #) + compute_posratpair(x-floor(x))
  ELSE (# num:=1,den:=1 #)/compute_posratpair(1/x)
  ENDIF MEASURE PosRatMeas(x)

aq: VAR [nat->rat]

rat_poly_to_int_rec(aq,n): RECURSIVE {ans:[# newpoly:[nat->rat],currgcd:posnat #] |
  (EXISTS (cp:posrat): FORALL (j:nat): ans`newpoly(j) = cp*aq(j)) AND
  (FORALL (j:upto(n)): rational_pred(ans`newpoly(j)) AND
             integer_pred(ans`newpoly(j)) AND
         divides(ans`currgcd,ans`newpoly(j)))} =
  IF n = 0 AND aq(0)=0 THEN (# newpoly:=aq,currgcd:=1 #)
  ELSIF n = 0 THEN
    LET thisden = compute_posratpair(abs(aq(0)))`den IN
      (# newpoly:= (LAMBDA (i:nat): thisden*aq(i)),
         currgcd:= abs(thisden*aq(0)) #)
  ELSIF aq(n) = 0 THEN rat_poly_to_int_rec(aq,n-1)
  ELSE
    LET currpoly = rat_poly_to_int_rec(aq,n-1),
thisden = compute_posratpair(abs(currpoly`newpoly(n)))`den
    IN  (# newpoly:=(LAMBDA (i:nat): thisden*(currpoly`newpoly(i))),
        currgcd:=compute_gcd(thisden*currpoly`newpoly(n),
                                   currpoly`currgcd) #)
  ENDIF MEASURE n

rat_poly_to_int(aq,n): {ai:[nat->int] | EXISTS (cp:posrat):
         FORALL (j:upto(n)): ai(j) = cp*aq(j) } =
  LET rptir = rat_poly_to_int_rec(aq,n),
      ppoly = rptir`newpoly,
      mgcd  = rptir`currgcd
  IN (LAMBDA (i:nat): IF i<=n THEN ppoly(i)/mgcd ELSE 0 ENDIF)

END clear_denominators

quality97%

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