isabelle: src/HOL/ex/Qsort.thy@89675b444abe (annotated)

8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	1	(* Title: HOL/ex/Qsort.thy
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	3	Author: Tobias Nipkow
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1994 TU Muenchen
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	Quicksort
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	Qsort = Sorting +
8590 89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	10
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	11	(Version one: higher-order)
8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	12	consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13
8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	14	recdef qsort "measure (size o snd)"
8524 f990040535c9 a possibly (?) more perspicous simprule in the "simpset" part paulson parents: 8414 diff changeset	15	simpset "simpset() addsimps [length_filter RS le_less_trans]"
8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	16
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	17	"qsort(le, []) = []"
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	18
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	19	"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	20	@ (x # qsort(le, [y:xs . le x y]))"
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	21
8590 89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	22
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	23	(Version two: type classes)
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	24	consts quickSort :: "('a::linorder) list => 'a list"
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	25
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	26	recdef quickSort "measure size"
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	27	simpset "simpset() addsimps [length_filter RS le_less_trans]"
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	28
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	29	"quickSort [] = []"
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	30
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	31	"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])"
89675b444abe added an order-sorted version of quickSort paulson parents: 8524 diff changeset	32
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	33	end

author	paulson
	Mon, 27 Mar 2000 17:04:03 +0200
changeset 8590	89675b444abe
parent 8524	f990040535c9
child 13159	2af7b94892ce
permissions	-rw-r--r--