# Theory Sorting

Up to index of Isabelle/HOL/ex

theory Sorting
imports Main Multiset
begin

    (*  Title:      HOL/ex/sorting.thy
        ID:         $Id: Sorting.thy,v 1.11 2005/04/22 15:32:03 paulson Exp $
        Author:     Tobias Nipkow
        Copyright   1994 TU Muenchen
    *)

    header{*Sorting: Basic Theory*}

    theory Sorting
    imports Main Multiset
    begin

    consts
      sorted1:: "('a => 'a => bool) => 'a list => bool"
      sorted :: "('a => 'a => bool) => 'a list => bool"

    primrec
      "sorted1 le [] = True"
      "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
                            sorted1 le xs)"

    primrec
      "sorted le [] = True"
      "sorted le (x#xs) = ((∀y ∈ set xs. le x y) & sorted le xs)"

    constdefs
      total  :: "('a => 'a => bool) => bool"
       "total r == (∀x y. r x y | r y x)"

      transf :: "('a => 'a => bool) => bool"
       "transf f == (∀x y z. f x y & f y z --> f x z)"

    (* Equivalence of two definitions of `sorted' *)

    lemma sorted1_is_sorted: "transf(le) ==> sorted1 le xs = sorted le xs";
    apply(induct xs)
     apply simp
    apply(simp split: list.split)
    apply(unfold transf_def);
    apply(blast)
    done

    lemma sorted_append [simp]:
     "sorted le (xs@ys) =
      (sorted le xs & sorted le ys & (∀x ∈ set xs. ∀y ∈ set ys. le x y))"
    by (induct xs, auto)

    end

lemma sorted1_is_sorted:

      transf le ==> sorted1 le xs = sorted le xs

lemma sorted_append:

      sorted le (xs @ ys) =
      (sorted le xs ∧ sorted le ys ∧ (∀x∈set xs. ∀y∈set ys. le x y))