Quelle multi_polylist.pvs Sprache: PVS

multi_polylist: THEORY
BEGIN

  IMPORTING util,reals@polynomials,
            multi_polynomial,
       MPoly

  MonoList: TYPE = list[nat]

  n,i        : VAR nat
  xvar       : VAR [nat->real]
  x,y        : VAR real
  ml,ml1,ml2 : VAR MonoList
  c      : VAR real

  maxnum(x,y:nat): {z:nat |
    z>=x AND z>=y AND (z=x OR z=y)} =
    IF x>=y THEN x ELSE y ENDIF

  max(ml1,ml2): RECURSIVE {ml |
    length[nat](ml)=maxnum(length[nat](ml1),length[nat](ml2)) AND
    FORALL (i:nat): i<length(ml) IMPLIES
             nth(ml,i) = IF null?(ml1) OR i>=length(ml1) THEN nth(ml2,i)
                      ELSIF null?(ml2) OR i>=length(ml2) THEN nth(ml1,i)
    ELSE maxnum(nth(ml1,i),nth(ml2,i)) ENDIF } =
    IF null?(ml1) THEN ml2
    ELSIF null?(ml2) THEN ml1
    ELSE cons(maxnum(car(ml1),car(ml2)),max(cdr(ml1),cdr(ml2)))
    ENDIF MEASURE length(ml1)+length(ml2)

  max_id: LEMMA max(ml,ml)=ml

  max_cdr: LEMMA null?(ml1) OR null?(ml2) OR cdr(max(ml1,ml2)) = max(cdr(ml1),cdr(ml2))

  max_sym: LEMMA max(ml1,ml2)=max(ml2,ml1)

  max_assoc: LEMMA max(ml,max(ml1,ml2))=max(max(ml,ml1),ml2)

  %%% A function that turns x(i)^n into a monomial

  varmono(i,n): RECURSIVE MonoList =
    IF i=0 THEN (: n :) ELSE cons(0,varmono(i-1,n)) ENDIF MEASURE i

  %%% Evaluation of monomials

  monolist_eval_rec(ml,c,i)(xvar): RECURSIVE
    {r : real | r = c*product(0,length(ml)-1,LAMBDA (k:nat):
         IF k<length(ml) THEN xvar(k+i)^nth(ml,k)
  ELSE 1 ENDIF) } =
    IF null?(ml) THEN c
    ELSE monolist_eval_rec(cdr(ml),c*xvar(i)^car(ml),i+1)(xvar)
    ENDIF
  MEASURE ml BY <<

  monolist_eval(ml)(xvar) : real =
    monolist_eval_rec(ml,1,0)(xvar)

  monolist_eval_prod: LEMMA
    monolist_eval(ml)(xvar) =
      product(0,length(ml)-1,LAMBDA (i:nat): IF i<length(ml) THEN xvar(i)^nth(ml,i)
                                      ELSE 1 ENDIF)

  %%% Multiplying monomials, which is really adding them

  monosum(ml1,ml2) : RECURSIVE {pml2:MonoList|
    FORALL (xvar): monolist_eval(pml2)(xvar)
      = monolist_eval(ml1)(xvar)*monolist_eval(ml2)(xvar)} =
  IF null?(ml1) THEN ml2
  ELSIF null?(ml2) THEN ml1
  ELSE cons(car(ml1)+car(ml2),monosum(cdr(ml1),cdr(ml2)))
  ENDIF
  MEASURE length(ml1)+length(ml2)

  ;+(ml1,ml2) : MACRO MonoList = monosum(ml1,ml2)

  %%% Multivariate Polynomials

  MultiPolyList: TYPE = list[[real,MonoList]]

  mpl,mpl1,mpl2 : VAR MultiPolyList

  meval(mpl)(xvar) : RECURSIVE real =
    IF null?(mpl) THEN 0
    ELSE LET (coe,mon) = car(mpl) IN
      coe*monolist_eval(mon)(xvar) + meval(cdr(mpl))(xvar)
    ENDIF MEASURE length(mpl)

  meval_sigma: LEMMA
    meval(mpl)(xvar) =
      sigma(0,length(mpl)-1,LAMBDA (i:nat): IF i<length(mpl) THEN
        nth(mpl,i)`1*monolist_eval(nth(mpl,i)`2)(xvar) ELSE 0 ENDIF)

  %%% Degree

  degree(mpl): RECURSIVE {ml |
    (NOT null?(mpl)) IMPLIES
    FORALL (i:below(length(mpl))):
      ml = max(nth(mpl,i)`2,ml) AND
      length(ml)>=length(nth(mpl,i)`2)} =
    IF null?(mpl) THEN (: :)
    ELSIF null?(cdr(mpl)) THEN car(mpl)`2
    ELSE max(car(mpl)`2,degree(cdr(mpl)))
    ENDIF MEASURE length(mpl)

  degree_zero: LEMMA
    null?(degree(mpl)) IMPLIES
    FORALL (i:nat): i<length(mpl) IMPLIES
      null?(nth(mpl,i)`2)

  %%% Converting to a Polynomial

  multipoly_to_poly(mpl)(t:nat)(v:nat)(d:nat): real =
    IF t<length(mpl) AND v<length(nth(mpl,t)`2) AND d=nth(nth(mpl,t)`2,v)
      THEN 1
    ELSIF t<length(mpl) AND null?(nth(mpl,t)`2) AND d=0 THEN 1
    ELSIF t<length(mpl) AND v>=length(nth(mpl,t)`2) AND d=0 THEN 1
    ELSE 0 ENDIF

  multipoly_to_mpoly(mpl): MPoly =
    IF length(mpl)=0 THEN mk_mpoly(LAMBDA (t:nat): LAMBDA (v:nat): LAMBDA (d:nat): 0,
                 LAMBDA (v:nat): 0, 1,LAMBDA (i:nat): 0)
    ELSE mk_mpoly(multipoly_to_poly(mpl),list2array[nat](0)(degree(mpl)),
   length(mpl),LAMBDA (i:nat): IF i<length(mpl) THEN nth(mpl,i)`1 ELSE 0 ENDIF) ENDIF

  %%% Simplifying

  mp_simp_rec(swiped,toswipe,ans:MultiPolyList,mono:MonoList,thiscoeff:real):
    RECURSIVE {mpl | FORALL (xvar): meval(mpl)(xvar)=meval(swiped)(xvar)+meval(toswipe)(xvar)
       +meval(ans)(xvar)+thiscoeff*monolist_eval(mono)(xvar)} =
    IF null?(swiped) AND null?(toswipe) AND thiscoeff/=0 THEN cons((thiscoeff,mono),ans)
    ELSIF null?(swiped) AND null?(toswipe) THEN ans
    ELSIF null?(toswipe) AND thiscoeff/=0 THEN
          mp_simp_rec(null,cdr(swiped),cons((thiscoeff,mono),ans),car(swiped)`2,car(swiped)`1)
    ELSIF null?(toswipe) THEN
          mp_simp_rec(null,cdr(swiped),ans,car(swiped)`2,car(swiped)`1)
    ELSIF mono = car(toswipe)`2 THEN mp_simp_rec(swiped,
                cdr(toswipe),ans,mono,car(toswipe)`1+thiscoeff)
    ELSE mp_simp_rec(cons(car(toswipe),swiped),cdr(toswipe),ans,mono,thiscoeff)
    ENDIF MEASURE lex2(length(swiped)+length(toswipe),length(toswipe))

  mp_simp(mpl): {mulist:MultiPolyList| meval(mpl)=meval(mulist)} =
    IF null?(mpl) THEN mpl
    ELSE mp_simp_rec(null,mpl,null,car(mpl)`2,0) ENDIF

  %%% Construction of MultyPolyList

  mpconst(c): MultiPolyList = (: (c, (: :)) :)

  mpmonom(c,i,n): MultiPolyList = (: (c,varmono(i,n)) :)

  mpvar(i): MultiPolyList = mpmonom(1,i,1)

  mpvarn(i,n): MultiPolyList = mpmonom(1,i,n)

  mpsum(mpl1,mpl2): {mpl|meval(mpl)=meval(mpl1)+meval(mpl2)} = mp_simp(append(mpl1,mpl2))

  ;+(mpl1,mpl2): MACRO MultiPolyList = mpsum(mpl1,mpl2)

  mpprod_rec(mpl1,mpl2): RECURSIVE {mpl |
    FORALL (xvar): meval(mpl)(xvar)=
            meval(mpl1)(xvar)*meval(mpl2)(xvar)} =
    IF null?(mpl1) THEN (: :)
    ELSIF null?(mpl2) THEN (: :)
    ELSIF null?(cdr(mpl1)) AND null?(cdr(mpl2))
      THEN (: (car(mpl1)`1*car(mpl2)`1,
               monosum(car(mpl1)`2,car(mpl2)`2)) :)
    ELSIF null?(cdr(mpl1)) THEN
      mpprod_rec(mpl1,cdr(mpl2))+mpprod_rec(mpl1,(: car(mpl2) :))
    ELSE mpprod_rec(cdr(mpl1),mpl2)+mpprod_rec((: car(mpl1) :),mpl2)
    ENDIF MEASURE length(mpl1)+length(mpl2)

  mpprod(mpl1,mpl2): {mpl |
    FORALL (xvar): meval(mpl)(xvar)=
            meval(mpl1)(xvar)*meval(mpl2)(xvar)} =
    mp_simp(mpprod_rec(mpl1,mpl2))

  ;*(mpl1,mpl2): MACRO MultiPolyList = mpprod(mpl1,mpl2)

  mpscal(c,mpl): RECURSIVE MultiPolyList =
    IF null?(mpl) THEN mpl
    ELSE cons((c*car(mpl)`1,car(mpl)`2),mpscal(c,cdr(mpl))) ENDIF
    MEASURE length(mpl)

  ;*(c,mpl): MACRO MultiPolyList = mpscal(c,mpl)

  mpminus(mpl1,mpl2): MultiPolyList =
    mpl1 + ((-1)*mpl2)

  ;-(mpl1,mpl2): MACRO MultiPolyList = mpminus(mpl1,mpl2)

  mppow(mpl,n): RECURSIVE MultiPolyList =
    IF n = 0 THEN (: (1,(: :)) :)
    ELSIF n = 1 THEN mpl
    ELSE mpl*mppow(mpl,n-1) ENDIF
    MEASURE n

  ;^(mpl,n): MACRO MultiPolyList = mppow(mpl,n)

  mpneg(mpl): MultiPolyList = (-1)*mpl

  ;-(mpl): MACRO MultiPolyList = mpneg(mpl)

  rnz: VAR nzreal

  mpdiv(mpl,rnz): MultiPolyList = (1/rnz)*mpl

  ;/(mpl,rnz): MACRO MultiPolyList = mpdiv(mpl,rnz)

  mpsq(mpl): MACRO MultiPolyList = mpl*mpl

  %%% Lemmas for rewriting

  multipolylist_eval: LEMMA
    meval(mpl)(xvar) = mpoly_eval(multipoly_to_mpoly(mpl),max(length(degree(mpl)),1))(xvar)

  multipolylist_const: LEMMA
    meval(mpconst(c))(xvar) = c

  multipolylist_monom: LEMMA
    meval(mpmonom(c,i,n))(xvar) = c*xvar(i)^n

  multipolylist_var: LEMMA
    meval(mpvar(i))(xvar) = xvar(i)

  multipolylist_varn: LEMMA
    meval(mpvarn(i,n))(xvar) = xvar(i)^n

  multipolylist_sum: LEMMA
    meval(mpl1+mpl2)(xvar) = meval(mpl1)(xvar)+meval(mpl2)(xvar)

  multipolylist_prod: LEMMA
    meval(mpl1*mpl2)(xvar) = meval(mpl1)(xvar)*meval(mpl2)(xvar)

  multipolylist_scal: LEMMA
    meval(c*mpl)(xvar) = c*meval(mpl)(xvar)

  multipolylist_pow: LEMMA
    meval(mpl^n)(xvar) = meval(mpl)(xvar)^n

  multipolylist_neg: LEMMA
    meval(-mpl)(xvar) = -meval(mpl)(xvar)

  multipolylist_minus: LEMMA
    meval(mpl1-mpl2)(xvar) = meval(mpl1)(xvar)-meval(mpl2)(xvar)

  multipolylist_div: LEMMA
    meval(mpl/rnz)(xvar) = meval(mpl)(xvar)/rnz

  multipolylist_sq: LEMMA
    meval(mpsq(mpl))(xvar) = sq(meval(mpl)(xvar))

END multi_polylist

quality76%

¤ Dauer der Verarbeitung: 0.17 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.