library Sorting2

%right_assoc __::__

spec Elem = 
  sort Elem
end

spec TotalOrder =
  sort Elem
  pred __<=__ : Elem * Elem
  forall x,y,z : Elem
  . x <= x                         %(reflexive)%
  . x <= z if x <= y /\ y <= z     %(transitive)%
  . x = y if x <= y /\ y <= x      %(antisymmetric)%
  . x <= y \/ y <= x               %(dichotomous)%
end


spec List[Elem] = 
  free type List[Elem] ::= [] | __::__(Elem; List[Elem])
  pred __eps__ : Elem * List[Elem]
  forall x,y:Elem; l:List[Elem]
  . not x eps []
  . x eps y::l <=> x=y \/ x eps l
end

spec ListAndOrder =
  List[TotalOrder]
end

spec PermutationAndOrdered =
  ListAndOrder
then
  preds is_ordered : List[Elem];
        permutation : List[Elem] * List[Elem]
  vars x,y:Elem; L,L1,L2:List[Elem]
  . is_ordered([])
  . is_ordered(x::[])
  . is_ordered(x::y::L) <=> x<=y /\ is_ordered(y::L)
  . permutation(L1,L2) <=> (forall x:Elem . x eps L1 <=>x eps L2)
end

spec SorterProps =
  PermutationAndOrdered
then
  op sorter : List[Elem]->List[Elem]
  var L:List[Elem]
  . is_ordered(sorter(L))
  . permutation(L,sorter(L))

spec Sorting =
  SorterProps
   hide is_ordered, permutation
end

spec InsertSortDef = 
  ListAndOrder
then
  ops insert : Elem*List[Elem] -> List[Elem];
      insert_sort : List[Elem]->List[Elem]
  vars x,y:Elem; L:List[Elem]
  . insert(x,[]) = x::[]
  . insert(x,y::L) = x::insert(y,L) when x<=y else y::insert(x,L)
  . insert_sort([]) = []
  . insert_sort(x::L) = insert(x,insert_sort(L))
end

spec InsertSort = 
  InsertSortDef
  hide insert
end

view InsertSortCorrectness : 
     Sorting to InsertSort =
    sorter |-> insert_sort
end

spec InsertSortAndPermOrderered =
  InsertSort
then %cons
  preds is_ordered : List[Elem];
        permutation : List[Elem] * List[Elem]
  vars x,y:Elem; L,L1,L2:List[Elem]
  . is_ordered([])
  . is_ordered(x::[])
  . is_ordered(x::y::L) <=> x<=y /\ is_ordered(y::L)
  . permutation(L1,L2) <=> (forall x:Elem . x eps L1 <=>x eps L2)
end

view v: SorterProps to InsertSortAndPermOrderered end