# Theory Sort

section ‹Locale Sort›
theory Sort
imports Main
"HOL-Library.Multiset"
begin
text ‹
First, we start from the definition of sorting algorithm. {\em What
are the basic properties that any sorting algorithm must satisfy? }
There are two
basic features any sorting algorithm must satisfy:
\begin{itemize}
\item The elements of sorted array must be in some order,
e.g. ascending or descending order. In this paper we are sorting in
ascending order.
$$sorted\ (sort\ \ l)$$
\item The algorithm does not change or delete elements of the given
array, e.g. the sorted array is the permutation of the input
array.
$$sort\ l\ <\sim \sim>\ l$$
\end{itemize}
›
locale Sort =
fixes sort :: "'a::linorder list ⇒ 'a list"
assumes sorted: "sorted (sort l)"
assumes permutation: "mset (sort l) = mset l"
end