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