Quellcode-Bibliothek permutations_seq.pvs

permutations_seq[T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
%  permutations_seq (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%
%    permutation?(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]): 
%                      bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii))))
%  
%
%------------------------------------------------------------------------


BEGIN

  A,B,A1,A2,A3: VAR finite_sequence[T]
  x, t: VAR T
  i,j: VAR nat

  in?(A)(x): bool = (EXISTS (ii: below(length(A))): seq(A)(ii) = x)


  permutation?(A,B): bool = (EXISTS (f: [below(length(A)) -> below(length(B))]): 
                     bijective?(f) AND 
                     (FORALL (ii: below(length(A))): seq(A)(ii) = seq(B)(f(ii))))

  IMPORTING finite_sets@finite_sets_card_eq, finite_sets@finite_sets_below

  perm_length   : LEMMA permutation?(A,B) IMPLIES length(A) = length(B)

  perm_reflexive: LEMMA permutation?(A,A)

  perm_symmetric: LEMMA permutation?(A,B) IMPLIES permutation?(B,A)

  perm_tran     : LEMMA permutation?(A1,A2) AND permutation?(A2,A3) 
                            IMPLIES permutation?(A1,A3)

  perm_in?      : LEMMA permutation?(A1,A2) IMPLIES 
                             (in?(A1)(x) = in?(A2)(x))




END permutations_seq