Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sincos_phase.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% 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

[ Seitenstruktur0.1Drucken  etwas mehr zur Ethik  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik