Quelle division_ring.pvs Sprache: PVS

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

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

BEGIN

   ASSUMING IMPORTING ring_with_one_def[T,+,*,zero,one], group_def,
                      division_ring_def[T,+,*,zero,one]

       fullset_is_division_ring: ASSUMPTION division_ring?(fullset[T])

   ENDASSUMING

   IMPORTING monoid_def, group_def, ring_nz_closed_def,
             division_ring_def[T,+,*,zero,one],
             ring_with_one[T,+,*,zero,one], ring_nz_closed[T,+,*,zero],
             group[nz_T,*,one]

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

% To bring elegance into this theory we define unary and binary minus and
% divide.
;
   recip: MACRO [nz_T->nz_T] = inv[nz_T,*,one];
   /: MACRO [T,nz_T->T]      = (LAMBDA (x:T,n0y:nz_T): x * recip(n0y))

   R:   VAR division_ring
   x,y: VAR T
   n0x,n0y,n0z: VAR nz_T

   division_ring_is       : LEMMA division_ring?(R)

   division_ring_is_ring_with_one:
                            JUDGEMENT division_ring SUBTYPE_OF ring_with_one

   division_ring_is_ring_nz_closed:
                            JUDGEMENT division_ring SUBTYPE_OF ring_nz_closed

   division_ring_is_group : LEMMA group?[nz_T,*,one](remove(zero,R))

   one_ne_zero            : LEMMA one /= zero
   cancel_times_right     : LEMMA (x * n0z = y * n0z) IFF x = y
   cancel_times_left      : LEMMA (n0z * x = n0z * y) IFF x = y
   idempotent_times       : LEMMA x * x = x IFF x = zero OR x = one
   recip_ne_zero          : LEMMA recip(n0x) /= zero
   nz_T_div_nz_T_is_nz_T  : JUDGEMENT /(n0x, n0y) HAS_TYPE nz_T
   div_simplify           : LEMMA n0x/n0x = one
   cancel_div_right       : LEMMA (x/n0z = y/n0z) IFF x = y
   cancel_div_left        : LEMMA (n0z/n0x = n0z/n0y) IFF n0x = n0y
   times_div_left         : LEMMA x * (y/n0z) = (x * y)/n0z
   div_eq_zero            : LEMMA x/n0z = zero IFF x = zero
   div_mult               : LEMMA (x/n0z) * n0z = x
   div_mult_left          : LEMMA x/n0z = y IFF x = y * n0z
   div_mult_right         : LEMMA y = x/n0z IFF y * n0z = x
   div_distributes        : LEMMA (x/n0z) + (y/n0z) = (x + y)/n0z
   div_distributes_minus  : LEMMA (x/n0z) - (y/n0z) = (x - y)/n0z
   div_div1               : LEMMA (x / (n0y / n0z)) = ((x * n0z) / n0y)
   div_div2               : LEMMA ((x / n0y) / n0z) = (x / (n0z * n0y))

   AUTO_REWRITE+ one_ne_zero            %% one /= zero
   AUTO_REWRITE+ div_simplify           %% n0x/n0x = one

END division_ring

quality96%

¤ Dauer der Verarbeitung: 0.14 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.