perm_props.pvs

perm_props[ T:TYPE ]: THEORY  % Welcome
 %Inputs: T - Type that makes up  entries
 %            of list

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%|  Facts about permutations of  |%
%|  lists that are needed for    |%
%|  subsequent theories          |%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Written By:                    AD

%-----     %
  BEGIN
%     -----%

%-------------------------------------------
%% Importing more_list_props and sorting
%  to have already established properits of
%  lists and definition of permutations
%-------------------------------------------

  IMPORTING sorting@sorting,
            structures@more_list_props[T]

%-------------------------------------------
%% Remove and entry from a nonempty list
%-------------------------------------------

  remove(l:(cons?[T]), i: below(length(l))):
  list[T]  = 
  append(IF i=0 THEN null[T]
  ELSE l^(0,i-1) ENDIF,l^(i+1, length(l)-1))

%-------------------------------------------
%% length and cdr properties of remove
%-------------------------------------------

  remove_length: LEMMA
  FORALL (l:(cons?[T]), i: below(length(l))):
  length(remove(l,i)) = length(l) - 1

  remove_cdr: LEMMA
  FORALL ((l:list[T] | length(l)>=2),
  (i: below(length(l)) | i>0)):
  cdr(remove(l,i)) = remove(cdr(l), i-1)

%-------------------------------------------
%% Splitting a list into three parts
%-------------------------------------------

  list_splitting_nth: LEMMA
  FORALL (l:(cons?[T]), i: below(length(l))):
  l = append(append(IF i=0 THEN null[T]
    ELSE l^(0,i-1) ENDIF,(: nth(l,i) :)),
    l^(i+1, length(l)-1))

%-------------------------------------------
%% Occurrence properties of remove
%-------------------------------------------

  occurrences_remove_not: LEMMA
  FORALL (l:(cons?[T]), i: below(length(l)), x:T):
  x/= nth(l, i) IMPLIES
  occurrences(l)(x) = occurrences(remove(l,i))(x)

  occurrences_remove: LEMMA 
  FORALL (l:(cons?[T]), i: below(length(l))):
  occurrences(l)(nth(l, i)) =
  occurrences(remove(l,i))(nth(l, i)) + 1

%-------------------------------------------
%% Showing invariant property under the
%  remove function, given certain conditions 
%-------------------------------------------

  remove_perm: LEMMA
  FORALL (l1, l2 : (cons?[T])):
  permutations(l1, l2)  IMPLIES
  EXISTS (i:below(length(l2))):
  (car(l1) = nth(l2,i) AND
  permutations(cdr(l1),remove(l2,i)))

  %~ The End  ~%
  END perm_props