equal
deleted
inserted
replaced
1 (* Title: HOL/ex/insort.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Insertion sort |
|
7 *) |
|
8 |
|
9 InSort = Sorting + |
|
10 |
|
11 consts |
|
12 ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list" |
|
13 insort :: "[['a,'a]=>bool, 'a list] => 'a list" |
|
14 |
|
15 primrec ins List.list |
|
16 ins_Nil "ins(f,x,[]) = [x]" |
|
17 ins_Cons "ins(f,x,y#ys) = if(f(x,y), x#y#ys, y#ins(f,x,ys))" |
|
18 primrec insort List.list |
|
19 insort_Nil "insort(f,[]) = []" |
|
20 insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))" |
|
21 end |
|