# HG changeset patch
# User nipkow
# Date 1190086966 -7200
# Node ID 17dbd993293d3723dbaa407268e959291c90397d
# Parent  a4b2eb0dd6737ef6c34f10a10d70f04a51c27359
Added function package to PreList
Added sorted/sort to List
Moved qsort from ex to Library

diff -r a4b2eb0dd673 -r 17dbd993293d src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Sep 17 16:36:45 2007 +0200
+++ b/src/HOL/Library/Library.thy	Tue Sep 18 05:42:46 2007 +0200
@@ -30,6 +30,7 @@
   Pretty_Char_chr
   Pretty_Int
   Primes
+  Quicksort
   Quotient
   Ramsey
   State_Monad
diff -r a4b2eb0dd673 -r 17dbd993293d src/HOL/Library/Quicksort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quicksort.thy	Tue Sep 18 05:42:46 2007 +0200
@@ -0,0 +1,44 @@
+(*  ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1994 TU Muenchen
+*)
+
+header{*Quicksort*}
+
+theory Quicksort
+imports Multiset
+begin
+
+context linorder
+begin
+
+function quicksort :: "'a list \<Rightarrow> 'a list" where
+"quicksort []     = []" |
+"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<^loc>\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<^loc>\<le>y])"
+by pat_completeness auto
+
+termination
+by (relation "measure size")
+   (auto simp: length_filter_le[THEN order_class.le_less_trans])
+
+end
+context linorder
+begin
+
+lemma quicksort_permutes [simp]:
+  "multiset_of (quicksort xs) = multiset_of xs"
+by (induct xs rule: quicksort.induct) (auto simp: union_ac)
+
+lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
+by(simp add: set_count_greater_0)
+
+lemma sorted_quicksort: "sorted(quicksort xs)"
+apply (induct xs rule: quicksort.induct)
+ apply simp
+apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
+apply (metis leD le_cases le_less_trans)
+done
+
+end
+
+end
diff -r a4b2eb0dd673 -r 17dbd993293d src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Mon Sep 17 16:36:45 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(*  Title:      HOL/ex/insort.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-*)
-
-header{*Insertion Sort*}
-
-theory InSort
-imports Sorting
-begin
-
-consts
-  ins    :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-primrec
-  "ins le x [] = [x]"
-  "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"
-
-primrec
-  "insort le [] = []"
-  "insort le (x#xs) = ins le x (insort le xs)"
-
-
-lemma multiset_ins[simp]:
- "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
-  by (induct xs) (auto simp: union_ac)
-
-theorem insort_permutes[simp]:
- "\<And>x. multiset_of (insort le xs) = multiset_of xs"
-  by (induct "xs") auto
-
-lemma set_ins [simp]: "set(ins le x xs) = insert x (set xs)"
-  by (simp add: set_count_greater_0) fast
-
-lemma sorted_ins[simp]:
- "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
-apply (induct xs)
-apply simp_all
-apply (unfold Sorting.total_def Sorting.transf_def)
-apply blast
-done
-
-theorem sorted_insort:
- "[| total(le); transf(le) |] ==>  sorted le (insort le xs)"
-by (induct xs) auto
-
-end
-
diff -r a4b2eb0dd673 -r 17dbd993293d src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Mon Sep 17 16:36:45 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(*  Title:      HOL/ex/Qsort.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-*)
-
-header{*Quicksort*}
-
-theory Qsort
-imports Sorting
-begin
-
-subsection{*Version 1: higher-order*}
-
-consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"
-
-recdef qsort "measure (size o snd)"
-    "qsort(le, [])   = []"
-    "qsort(le, x#xs) = qsort(le, [y\<leftarrow>xs . ~ le x y]) @ [x] @
-		       qsort(le, [y\<leftarrow>xs . le x y])"
-(hints recdef_simp: length_filter_le[THEN le_less_trans])
-
-lemma qsort_permutes [simp]:
-     "multiset_of (qsort(le,xs)) = multiset_of xs"
-by (induct le xs rule: qsort.induct) (auto simp: union_ac)
-
-lemma set_qsort [simp]: "set (qsort(le,xs)) = set xs";
-by(simp add: set_count_greater_0)
-
-lemma sorted_qsort:
-     "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
-apply (induct le xs rule: qsort.induct)
- apply simp
-apply simp
-apply(unfold Sorting.total_def Sorting.transf_def)
-apply blast
-done
-
-
-subsection{*Version 2:type classes*}
-
-consts quickSort :: "('a::linorder) list => 'a list"
-
-recdef quickSort "measure size"
-    "quickSort []   = []"
-    "quickSort (x#l) = quickSort [y\<leftarrow>l. ~ x\<le>y] @ [x] @ quickSort [y\<leftarrow>l. x\<le>y]"
-(hints recdef_simp: length_filter_le[THEN le_less_trans])
-
-lemma quickSort_permutes[simp]:
- "multiset_of (quickSort xs) = multiset_of xs"
-by (induct xs rule: quickSort.induct) (auto simp: union_ac)
-
-lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
-by(simp add: set_count_greater_0)
-
-theorem sorted_quickSort: "sorted (op \<le>) (quickSort xs)"
-by (induct xs rule: quickSort.induct, auto)
-
-end
diff -r a4b2eb0dd673 -r 17dbd993293d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Mon Sep 17 16:36:45 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Sep 18 05:42:46 2007 +0200
@@ -32,8 +32,6 @@
   "CTL",
   "Arith_Examples",
   "BT",
-  "InSort",
-  "Qsort",
   "MergeSort",
   "Puzzle",
   "Lagrange",