ex/InSort.thy
author nipkow
Wed, 23 Feb 1994 10:05:35 +0100
changeset 46 a73f8a7784bd
child 48 21291189b51e
permissions -rw-r--r--
some more sorting algorithms
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     1
(*  Title: 	HOL/ex/insort.thy
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     2
    ID:         $Id$
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     3
    Author: 	Tobias Nipkow
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     5
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     6
Insertion sort
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     7
*)
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     8
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
     9
InSort  =  Sorting +
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    10
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    11
consts
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    12
  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    13
  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    14
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    15
rules
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    16
  ins_Nil  "ins(f,x,[]) = [x]"
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    17
  ins_Cons "ins(f,x,Cons(y,ys)) =   \
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    18
\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    19
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    20
  insort_Nil  "insort(f,[]) = []"
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    21
  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
a73f8a7784bd some more sorting algorithms
nipkow
parents:
diff changeset
    22
end