# HG changeset patch
# User haftmann
# Date 1288783233 -3600
# Node ID 131cf8790a1c4f195380ea77026cfa2cd6476a45
# Parent  e484bacfbe641fea9fa101953090dda4bc3e36d6
moved theory Quicksort from Library/ to ex/

diff -r e484bacfbe64 -r 131cf8790a1c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Nov 03 12:20:33 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 03 12:20:33 2010 +0100
@@ -431,7 +431,7 @@
   Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
   Library/Preorder.thy Library/Product_Vector.thy			\
   Library/Product_ord.thy Library/Product_plus.thy			\
-  Library/Quickcheck_Types.thy Library/Quicksort.thy			\
+  Library/Quickcheck_Types.thy						\
   Library/Quotient_List.thy Library/Quotient_Option.thy			\
   Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
   Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
@@ -1023,13 +1023,14 @@
   ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
   ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy		\
   ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
-  ex/Quickcheck_Lattice_Examples.thy ex/ROOT.ML ex/Recdefs.thy		\
-  ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
-  ex/SAT_Examples.thy ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy	\
-  ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy	\
-  ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy			\
-  ex/While_Combinator_Example.thy ex/document/root.bib			\
-  ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
+  ex/Quickcheck_Lattice_Examples.thy ex/Quicksort.thy ex/ROOT.ML	\
+  ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
+  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
+  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
+  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
+  ex/Unification.thy ex/While_Combinator_Example.thy			\
+  ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
+  ex/svc_test.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
 
diff -r e484bacfbe64 -r 131cf8790a1c src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Nov 03 12:20:33 2010 +0100
+++ b/src/HOL/Library/Library.thy	Wed Nov 03 12:20:33 2010 +0100
@@ -45,7 +45,6 @@
   Polynomial
   Preorder
   Product_Vector
-  Quicksort
   Quotient_List
   Quotient_Option
   Quotient_Product
diff -r e484bacfbe64 -r 131cf8790a1c src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Wed Nov 03 12:20:33 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-*)
-
-header {* Quicksort *}
-
-theory Quicksort
-imports Main Multiset
-begin
-
-context linorder
-begin
-
-fun quicksort :: "'a list \<Rightarrow> 'a list" where
-  "quicksort []     = []"
-| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
-
-lemma [code]:
-  "quicksort []     = []"
-  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
-  by (simp_all add: not_le)
-
-lemma quicksort_permutes [simp]:
-  "multiset_of (quicksort xs) = multiset_of xs"
-  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
-
-lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
-  by (simp add: set_count_greater_0)
-
-lemma sorted_quicksort: "sorted (quicksort xs)"
-  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
-
-theorem quicksort_sort [code_unfold]:
-  "sort = quicksort"
-  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
-
-end
-
-end
diff -r e484bacfbe64 -r 131cf8790a1c src/HOL/ex/Quicksort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Quicksort.thy	Wed Nov 03 12:20:33 2010 +0100
@@ -0,0 +1,39 @@
+(*  Author:     Tobias Nipkow
+    Copyright   1994 TU Muenchen
+*)
+
+header {* Quicksort with function package *}
+
+theory Quicksort
+imports Main Multiset
+begin
+
+context linorder
+begin
+
+fun quicksort :: "'a list \<Rightarrow> 'a list" where
+  "quicksort []     = []"
+| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+
+lemma [code]:
+  "quicksort []     = []"
+  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+  by (simp_all add: not_le)
+
+lemma quicksort_permutes [simp]:
+  "multiset_of (quicksort xs) = multiset_of xs"
+  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
+
+lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
+  by (simp add: set_count_greater_0)
+
+lemma sorted_quicksort: "sorted (quicksort xs)"
+  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
+
+theorem sort_quicksort:
+  "sort = quicksort"
+  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
+
+end
+
+end
diff -r e484bacfbe64 -r 131cf8790a1c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Nov 03 12:20:33 2010 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Nov 03 12:20:33 2010 +0100
@@ -66,7 +66,8 @@
   "Execute_Choice",
   "Summation",
   "Gauge_Integration",
-  "Dedekind_Real"
+  "Dedekind_Real",
+  "Quicksort"
 ];
 
 HTML.with_charset "utf-8" (no_document use_thys)