ex/insort.thy

+(*  Title: 	HOL/ex/insort.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Insertion sort
+*)
+
+InSort  =  Sorting +
+
+consts
+  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
+  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
+
+rules
+  ins_Nil  "ins(f,x,[]) = [x]"
+  ins_Cons "ins(f,x,Cons(y,ys)) =   \
+\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+
+  insort_Nil  "insort(f,[]) = []"
+  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+end