Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: field.pvs Sprache: PVS

Original von: PVS^©

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

field[T:Type+,+,*:[T,T->T],zero,one:T]: THEORY

BEGIN

   ASSUMING IMPORTING division_ring_def[T,+,*,zero,one],
                      integral_domain_def[T,+,*,zero],
                      field_def[T,+,*,zero,one]

       fullset_is_field: ASSUMPTION field?(fullset[T])

   ENDASSUMING

   IMPORTING abelian_group,
             division_ring_def[T,+,*,zero,one],
             field_def[T,+,*,zero,one],
             division_ring[T,+,*,zero,one],
             integral_domain[T,+,*,zero]

   field: NONEMPTY_TYPE = (field?) CONTAINING fullset[T]

   nz_star:[nz_T,nz_T->nz_T]
                     = restrict[[T,T],[nz_T[T,+,*,zero],nz_T[T,+,*,zero]],T](*)

   F:           VAR field
   S:           VAR set[T]
   x,y:         VAR T
   n0x,n0y,n0z: VAR nz_T

   field_is_division_ring:   JUDGEMENT field SUBTYPE_OF division_ring
   field_is_integral_domain: JUDGEMENT field SUBTYPE_OF integral_domain
   field_is_abelian_group:
                         LEMMA abelian_group?[nz_T,nz_star,one](remove(zero,F))

   mult_div:        LEMMA n0z * (x/n0z) = x
   times_div_right: LEMMA (x/n0z) * y = (x * y)/n0z
   div_times:       LEMMA (x/n0x) * (y/n0y) = (x*y)/(n0x*n0y)
   cross_mult:      LEMMA (x/n0x = y/n0y) IFF (x * n0y = y * n0x)
   add_div:         LEMMA (x/n0x) + (y/n0y) = (x * n0y + y * n0x)/(n0x * n0y)
   minus_div1:      LEMMA (x/n0x) - (y/n0y) = (x * n0y - y * n0x)/(n0x * n0y)

   sq_div:          LEMMA sq(x/n0z) = sq(x)/sq(n0z)

END field

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.