sorting_tutorial_1: THEORY
BEGIN

%%% 
%%% We use the parameterized 'list' type from the PVS prelude,
%%% instantiated for integer elements.  The 'list' theory  has functions
%%% defined for 'length', and other basic properties. 
%%%
slist: TYPE = list[int]
l,l1,l2,l3: VAR slist
i,j,k: VAR int
m, n: nat

%%%
%%% A list is sorted if its elements are in order.
%%%

sorted?(l): RECURSIVE bool =
  CASES l OF
   null: true,
   cons(i, tl): CASES tl OF
                 null: true,
                 cons(j, ttl): i <= j and sorted?(tl)
                ENDCASES
  ENDCASES
  MEASURE l by <<

%%%
%%% But sorting is not quite enough, if there are repeated elements
%%% in the list.  Sorting algorthms should not change the _content_
%%% of a list, meaning that if an integer i occurs N times before
%%% the list is sorted, it must occur N times afterward.
%%%
%%% You could either exclude this possibility or allow it.  Either
%%% way, there is going to be additional work to do.
%%%
%%% One list is a _permutation_ of another if contain the same elements
%%% in the same number of occurances.
%%% 

occurrences(i, l): RECURSIVE nat =
  CASES l OF
    null:       0,
    cons(j, tl): IF (i = j)
                THEN 1 + occurrences(i, tl)
                ELSE occurrences(i, tl)
                ENDIF
  ENDCASES
  MEASURE l by <<

permutation?(l1, l2): bool =
     (forall (i): occurrences(i, l1) = occurrences(i, l2))

%%%
%%% A recursive form of Bubble Sort
%%%

BB(j, l): RECURSIVE slist =
  CASES l OF
    null: cons(j, null),
    cons(i, tl): 
       IF j <= i
       THEN cons(j, BB(i, tl))
       ELSE cons(i, BB(j, tl))
       ENDIF
  ENDCASES
  MEASURE l BY <<

Bsort(l): RECURSIVE slist =
  CASES l OF
    null: null,
    cons(i, tl): BB(i, Bsort(tl))
  ENDCASES
  MEASURE l BY <<

%%%
%%% What do we need to know about "BB" in order to prove
%%% xBsort_correct, below?  I've left a partial proof to
%%% show how a proof attempt might expose the needed lemmas.
%%% The problem, as always, is to make the appropriate
%%% generalizations.
%%%
%%% NOTE: Still more lemmas may be needed to make this
%%% all to through more simply.  Step through the partial proofs
%%% and compare the residual subgoals.
%%%

xBsort_correct: THEOREM permutation?(l, Bsort(l)) AND sorted?(Bsort(l))

BB_preserves_permutation: LEMMA
   permutation?(l1, l2) IMPLIES permutation?(cons(k, l1), BB(k, l2))

BB_preserves_sorted: LEMMA
   sorted?(l) IMPLIES sorted?(BB(k, l))

Bsort_correct: THEOREM
   permutation?(l, Bsort(l)) AND sorted?(Bsort(l))


END sorting_tutorial_1