| products/sources/formale Sprachen/Cobol/Test-Suite/SQL M/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: ring_with_one.pvs Sprache: PVS
|
%------------------------------------------------------------------------------
% Rings with one % % Author: David Lester, Manchester University & NIA % Rick Butler % % Version 1.0 3/1/02 % Version 1.1 12/3/03 New library structure % Version 1.2 5/5/04 Reworked for definition files DRL %------------------------------------------------------------------------------ ring_with_one[T:Type+,+,*:[T,T->T],zero,one:T]: THEORY BEGIN ASSUMING IMPORTING ring_def[T,+,*,zero], ring_with_one_def[T,+,*,zero,one] fullset_is_ring_with_one: ASSUMPTION ring_with_one?(fullset[T]) ENDASSUMING IMPORTING ring_with_one_def[T,+,*,zero,one], ring[T,+,*,zero], monoid[T,*,one], operator_defs_more[T] ring_with_one: NONEMPTY_TYPE = (ring_with_one?) CONTAINING fullset[T] R: VAR ring_with_one x,y: VAR T one_times : LEMMA one * x = x times_one : LEMMA x * one = x unique_left_identity : LEMMA (FORALL x: y*x = x) IFF y = one unique_right_identity : LEMMA (FORALL x: x*y = x) IFF y = one minus_one_times : LEMMA (-one)*x = -x times_minus_one : LEMMA x*(-one) = -x minus_one_sq_is_one : LEMMA (-one)*(-one) = one ring_with_one_is_ring : JUDGEMENT ring_with_one SUBTYPE_OF ring ring_with_one_is_monoid: JUDGEMENT ring_with_one SUBTYPE_OF monoid[T,*,one] AUTO_REWRITE+ one_times % one * x = x AUTO_REWRITE+ times_one % x * one = x AUTO_REWRITE+ minus_one_times % (-one)*x = -x AUTO_REWRITE+ times_minus_one % x*(-one) = -x AUTO_REWRITE+ minus_one_sq_is_one % (-one)*(-one) = one END ring_with_one [ zur Elbe Produktseite wechseln0.24Quellennavigators Analyse erneut starten ] |