Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: rs_integral_prep.prf Sprache: PVS

Original von: PVS^©

%% examples4Q.pvs
%%
%% These examples only deal with rational expressions, for that reason the theory
%% just imports strategies4Q.
%%

examples4Q : theory
BEGIN

  IMPORTING strategies4Q

  x,y : var real

  %%%% Examples of numerical

  zero_to_one_quarter : LEMMA
    x ## [|0,1|] IMPLIES
    x*(1-x) ## [|0.0000, 0.2501|]
%% The expression (! 1 1) refers to formula 1, 1st term, i.e., x*(1-x)
%|- zero_to_one_quarter : PROOF
%|- (then (skeep) (numerical (! 1 1) :precision 4 :maxdepth 20 :verbose? t))
%|- QED

  x0,x1,x2,x3,x4,x5,x6,x7 : VAR real

  Heart(x0,x1,x2,x3,x4,x5,x6,x7): MACRO real =
    -x0*x5^3+3*x0*x5*x6^2-x2*x6^3+3*x2*x6*x5^2-x1*x4^3+3*x1*x4*x7^2-x3*x7^3+3*x3*x7*x4^2-0.9563453

  hdp_mm: LEMMA
    -0.1 <= x0 AND x0 <= 0.4 AND
     0.4 <= x1  AND x1 <= 1 AND
    -0.7 <= x2 AND x2 <= -0.4 AND
    -0.7 <= x3 AND x3 <= 0.4 AND
     0.1 <= x4  AND x4 <= 0.2 AND
    -0.1 <= x5 AND x5 <= 0.2 AND
    -0.3 <= x6 AND x6 <= 1.1 AND
    -1.1 <= x7 AND x7 <= -0.3 IMPLIES
     Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [|-1.852, 1.518|]

%% The expression (! 1 1) refers to formula 1, 1st term, i.e., polynomial Heart
%|- hdp_mm : PROOF
%|- (then (skeep) (numerical (! 1 1) :verbose? t))
%|- QED

  %%%% Examples of interval

  hdp_minmax: LEMMA
    -0.1 <= x0 AND x0 <= 0.4 AND
     0.4 <= x1  AND x1 <= 1 AND
    -0.7 <= x2 AND x2 <= -0.4 AND
    -0.7 <= x3 AND x3 <= 0.4 AND
     0.1 <= x4  AND x4 <= 0.2 AND
    -0.1 <= x5 AND x5 <= 0.2 AND
    -0.3 <= x6 AND x6 <= 1.1 AND
    -1.1 <= x7 AND x7 <= -0.3 IMPLIES
     Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [| -1.76, 1.46 |]

%|- hdp_minmax : PROOF
%|- (then (skeep) (interval))
%|- QED

  common_point: LEMMA
    EXISTS (x,y,z:real): abs(x) <= 10 AND abs(y) <= 10 AND z ## [|0,1/2|] AND
      LET x2 = x^2,
          y2 = y^2 IN
        x2-2*x+1+y2-2*y+1<1 AND x2 + y2 < 3-2*y+0.01

%|- common_point : PROOF (interval :verbose? t) QED

   Eps : posreal = 0.0001

   simple_ite : LEMMA
     FORALL (x:real | x ## [| 0, 10 |]) :
       IF x <= 1 THEN sq(x) <= x+Eps
       ELSE sq(x) >= x-Eps
       ENDIF

%|- simple_ite : PROOF
%|- (interval)
%|- QED

END examples4Q

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.