SSL permutation.pvs   Interaktion und
PortierbarkeitPVS

permutation[N: nat]: THEORY
%----------------------------------------------------------------------------
% the theory of bijective mappings from below(N) to below(N)
%
% Author: Alfons Geser, National Institute of Aerospace, Hampton, VA, 2003
%----------------------------------------------------------------------------
BEGIN

  permutation: TYPE+ = {pi: [below(N) -> below(N)] | bijective?(pi)}
               CONTAINING id

  i,j,k  : VAR below(N)
  m      : VAR below(N+1)
  pi, rho: VAR permutation

  inverse_id         : LEMMA N > 0 IMPLIES inverse[below(N),below(N)](id) = id

  inverse_composition: LEMMA N > 0 IMPLIES inverse(pi o rho) = inverse(rho) o inverse(pi)

  transpose(i,j): permutation = 
          LAMBDA k: IF k = j THEN i ELSIF k = i THEN j ELSE k ENDIF

  involutorian_transpose: LEMMA transpose(i,j)(transpose(i,j)(k)) = k

END permutation