Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: clear_denominators.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.