author | wenzelm |
Thu, 01 Jul 1999 21:19:45 +0200 | |
changeset 6874 | 747f656e04ec |
parent 5184 | 9b8547a9496a |
child 8422 | 6c6a5410a9bd |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/ex/insort.thy |
969 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
Insertion sort |
|
7 |
*) |
|
8 |
||
9 |
InSort = Sorting + |
|
10 |
||
11 |
consts |
|
1376 | 12 |
ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list |
13 |
insort :: [['a,'a]=>bool, 'a list] => 'a list |
|
969 | 14 |
|
5184 | 15 |
primrec |
1896 | 16 |
"ins f x [] = [x]" |
17 |
"ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" |
|
5184 | 18 |
primrec |
1896 | 19 |
"insort f [] = []" |
20 |
"insort f (x#xs) = ins f x (insort f xs)" |
|
969 | 21 |
end |
1896 | 22 |