|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
real_lebesgue_scaf.pvs
Sprache: PVS
Original von: PVS©
|
|
%% Examples of use of ProofLite 6.0
%% Cesar Munoz
%% http://shemesh.larc.nasa.gov/people/cam/ProofLite
%% NASA LaRC
prooflite_examples : THEORY
BEGIN
% INSTRUCTIONS (Interactive Mode)
% - Typecheck this file and use the command
% M-x load-prelude-library ProofLite
%
% - To install all the ProofLite scripts type
% M-x install-prooflite-scripts-theory (C-c it)
%
% - To install a particular ProofLite script, place the cursor on the script
% and type
% M-x install-prooflite-script (C-c ip)
%
% CAVEATS:
% By default proofs are not overridden. To force overriding use the commands:
% - M-x install-prooflite-scripts-theory! (C-c !t)
% - M-x install-prooflite-script! (C-c !p)
%
% INSTRUCTIONS (Batch Mode)
%
% Run the proveit utility:
% <pvs-dir>/proveit prooflite_examples
%
a,b : VAR real
nza : VAR nzreal
l1: LEMMA
a*a >= 0
% One line proof scripts
%|- l1 : PROOF (grind) QED
l2: LEMMA
(nza/2)*(2/nza) = 1
% Multiple line proof scripts
%|- l2 : PROOF
%|- (then (skosimp)
%|- (grind))
%|- QED
l3: LEMMA
a*a >= 0
l4: LEMMA
(nza/2)*(2/nza) = 1
% Sharing proof scripts
%|- l3 : PROOF
%|- l4 : PROOF
%|- (grind)
%|- QED
l3a: LEMMA
a*a >= 0
l4a: LEMMA
(nza/2)*(2/nza) = 1
% Proof scripts for name-matching lemmas
%|- l*a : PROOF
%|- (grind)
%|- QED
l_5_6 : LEMMA
EXISTS (a) : 5 < a AND a < 6
l_6_7 : LEMMA
EXISTS (a) : 6 < a AND a < 7
% Proof macros
%|- l_*_* : PROOF
%|- (then (skip-msg "Proving Lemma: $0")
%|- (inst 1 "$1 + ($2 - $1)/2")
%|- (grind))
%|- QED
l_8 : LEMMA
EXISTS (a,b) : a+b = 8
l_9 : LEMMA
EXISTS (a,b) : a+b = 9
% Parametric proofs
%|- l_8[2;6] : PROOF
%|- l_9[4;5] : PROOF
%|- (then (skip-msg "Proving Lemma: $0")
%|- (inst 1 "#1" "#2")
%|- (grind))
%|- QED
END prooflite_examples
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
