library Sorting

from Basic/StructuredDatatypes get Int
from Basic/StructuredDatatypes get List

spec Sort =
  List[Int fit sort Elem |-> Int] with sort List[Int] |-> List
then

  pred isSorted: List
  forall l:List
  . isSorted(l) if #(l) <= 1
  . (isSorted(l) <=>   
       first(l) <= first(rest(l)) /\ isSorted(rest(l))
    ) if #(l) > 1

  pred __hasSameOccurencesAs__: List * List
  forall l,k: List
  . l hasSameOccurencesAs k
    <=>
    forall x: Int .
       freq(l,x) = freq(k,x)    

  op sortFunction: List -> List
  forall l: List
  . isSorted(sortFunction(l))  /\ 
    l hasSameOccurencesAs sortFunction(l)

end

spec InsertSort =
  List[Int fit sort Elem |-> Int] with sort List[Int] |-> List
then

  op insert: Int * List -> List
  forall x,y: Int; l: List
  . insert(x,[]   ) = x :: [] 
  . insert(x, y::l) =   x :: y :: l    when x < y
                else    y :: insert(x,l)

  op insertSort: List -> List
  forall x,y: Int; l:List
  . insertSort ( [] ) = []
  . insertSort ( x :: [] ) = x ::[]  
  . insertSort ( x :: y :: l ) = 
         insert(x, insertSort( y :: l ))

end

view InsertSort_is_correct:
  {InsertSort reveal op insertSort} to Sort 
= 
  op insertSort |-> sortFunction
end