sort_inversions[N: posnat, T: TYPE, <= : (total_order?[T]) ]: THEORY
%----------------------------------------------------------------------------
% inversions, i.e., index pairs i < j such that A(i) > A(j)
% are witnessses that array A is not sorted.
% transposition of adjacent elements A(j) > A(j+1) decrease
% the number of inversions. This is the basis of bubble sort.
%
% Author: Alfons Geser, National Institute of Aerospace, 2003
%----------------------------------------------------------------------------

BEGIN

  index_pair: TYPE = [below(N),below(N)]

  IMPORTING sort_array[N,T,<=],
            finite_sets[index_pair],
            permutation_ops[N]

  A    : VAR [below(N) -> T]
  inv  : VAR finite_set[index_pair]
  i,j,k: VAR below(N)
  x    : VAR T

  % to discharge the TCC for inversions
  finite_inversions: LEMMA
    is_finite[index_pair]({(i, j) | i < j & NOT A(i) <= A(j)})

  % the set of inversions, i.e, of index pairs (i,j) such that
  % A(i) and A(j) are not in sorted order
  inversions(A): finite_set[index_pair] =
    {(i,j) | i < j & NOT A(i) <= A(j)}

  pi: VAR permutation

  % to discharge the TCC for ap(pi,inv) below
  finite_ap: LEMMA
    is_finite[index_pair](LAMBDA (i, j): inv(pi(i), pi(j)))

  % apply a permutation pi to a set of index pairs
  ap(pi,inv): finite_set[index_pair] = LAMBDA (i,j): inv(pi(i),pi(j))

  % applying a permutation does not change the number of index pairs
  card_ap: LEMMA
    card[index_pair](ap(pi,inv)) = card[index_pair](inv)

  inversions_transpose: LEMMA
    j < N-1 & NOT A(j) <= A(j+1) =>
      inversions(A o transpose(j,j+1)) =
        ap(transpose(j,j+1),remove((j,j+1),inversions(A)))

  % main results:
  % 1) if (j,j+1) is an inversion then exchanging j with j+1 decreases
  %    the number of inversions by one
  % 2) if there are no inversions then A is sorted
  % 3) if there are inversions then there are inversions of the form (j,j+1)

  card_inversions_transpose: THEOREM
    j < N-1 & NOT A(j) <= A(j+1) =>
      card(inversions(A)) = 1 + card(inversions(A o transpose(j,j+1)))

  sorted_iff_no_inversions: THEOREM
    sorted?(A) <=> empty?(inversions(A))

  d: VAR nat

  successive_inversion_lem: LEMMA
    (EXISTS i: i < i+d & i+d < N & NOT A(i) <= A(i+d)) =>
    (EXISTS j: j < N-1 & NOT A(j) <= A(j+1))

  successive_inversion_exists: THEOREM
    NOT sorted?(A) => EXISTS j: j < N-1 & NOT A(j) <= A(j+1)
 
END sort_inversions