Impressum zn.pvs  Interaktion und
Portierbarkeitunbekannt

zn[N: posnat]: THEORY
%------------------------------------------------------------------------
% Integer Groups
%
%     Author:     Rick Butler, NASA Langley Research Center
%
% Goal: show that Z_n is isomorphic to Z/nZ             
%
%     Version 1.0            12/14/07
%------------------------------------------------------------------------
BEGIN
   
  IMPORTING group, group_rew

  ++(a,b: below(N)): below(N) = mod(a+b,N)  

  floor_help: LEMMA FORALL (x: below(N)): floor(x / N) = 0

  AUTO_REWRITE+ floor_help

  Z_group: LEMMA group?[int, +, 0](fullset[int]);

  Z: group[int,+,0] = fullset[int]

  Z_prep: LEMMA group?[below(N), ++, 0](fullset[below(N)]);


  Z_: group[below(N),++,0] = fullset[below(N)]


%%  IMPORTING ints@primes

%%  zn_prime_field: LEMMA prime?(N) IMPLIES field?[below(N),++,0] = fullset[below(N)]



  nZ_TYPE: TYPE = {x: int | EXISTS (k: int): x = k*N}

  nZ_plus(x,y: nZ_TYPE): nZ_TYPE = x + y

  nZ_prep: LEMMA group?[nZ_TYPE, nZ_plus, 0](fullset[(nZ_TYPE)]);

  nZ: group[nZ_TYPE, +, 0] = fullset[nZ_TYPE]


  IMPORTING factor_groups

  nZ_normal: LEMMA normal_subgroup?(nZ,Z)

%% THE FOLLOWING currently breaks PVS 4.1 with
%%    Break: set-type-for-application-parameters

%  Z_fact_test: LEMMA FORALL (G: factor_type(Z,nZ)): group?[factor_type(Z,nZ),mult(Z,nZ),nZ](G)

  Z_fact_test: LEMMA group?[factor_type(Z,nZ),mult(Z,nZ),nZ](Z/nZ)

   
END zn