Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle field.pvs Sprache: 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

quality95%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.