moved theory Quicksort from Library/ to ex/
authorhaftmann
Wed Nov 03 12:20:33 2010 +0100 (2010-11-03)
changeset 40349131cf8790a1c
parent 40348 e484bacfbe64
child 40350 1ef7ee8dd165
moved theory Quicksort from Library/ to ex/
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Quicksort.thy
src/HOL/ex/Quicksort.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Nov 03 12:20:33 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Nov 03 12:20:33 2010 +0100
     1.3 @@ -431,7 +431,7 @@
     1.4    Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
     1.5    Library/Preorder.thy Library/Product_Vector.thy			\
     1.6    Library/Product_ord.thy Library/Product_plus.thy			\
     1.7 -  Library/Quickcheck_Types.thy Library/Quicksort.thy			\
     1.8 +  Library/Quickcheck_Types.thy						\
     1.9    Library/Quotient_List.thy Library/Quotient_Option.thy			\
    1.10    Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
    1.11    Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
    1.12 @@ -1023,13 +1023,14 @@
    1.13    ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
    1.14    ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy		\
    1.15    ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
    1.16 -  ex/Quickcheck_Lattice_Examples.thy ex/ROOT.ML ex/Recdefs.thy		\
    1.17 -  ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
    1.18 -  ex/SAT_Examples.thy ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy	\
    1.19 -  ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy	\
    1.20 -  ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy			\
    1.21 -  ex/While_Combinator_Example.thy ex/document/root.bib			\
    1.22 -  ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
    1.23 +  ex/Quickcheck_Lattice_Examples.thy ex/Quicksort.thy ex/ROOT.ML	\
    1.24 +  ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
    1.25 +  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.26 +  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
    1.27 +  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
    1.28 +  ex/Unification.thy ex/While_Combinator_Example.thy			\
    1.29 +  ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
    1.30 +  ex/svc_test.thy
    1.31  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    1.32  
    1.33  
     2.1 --- a/src/HOL/Library/Library.thy	Wed Nov 03 12:20:33 2010 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Wed Nov 03 12:20:33 2010 +0100
     2.3 @@ -45,7 +45,6 @@
     2.4    Polynomial
     2.5    Preorder
     2.6    Product_Vector
     2.7 -  Quicksort
     2.8    Quotient_List
     2.9    Quotient_Option
    2.10    Quotient_Product
     3.1 --- a/src/HOL/Library/Quicksort.thy	Wed Nov 03 12:20:33 2010 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,39 +0,0 @@
     3.4 -(*  Author:     Tobias Nipkow
     3.5 -    Copyright   1994 TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -header {* Quicksort *}
     3.9 -
    3.10 -theory Quicksort
    3.11 -imports Main Multiset
    3.12 -begin
    3.13 -
    3.14 -context linorder
    3.15 -begin
    3.16 -
    3.17 -fun quicksort :: "'a list \<Rightarrow> 'a list" where
    3.18 -  "quicksort []     = []"
    3.19 -| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    3.20 -
    3.21 -lemma [code]:
    3.22 -  "quicksort []     = []"
    3.23 -  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    3.24 -  by (simp_all add: not_le)
    3.25 -
    3.26 -lemma quicksort_permutes [simp]:
    3.27 -  "multiset_of (quicksort xs) = multiset_of xs"
    3.28 -  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
    3.29 -
    3.30 -lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    3.31 -  by (simp add: set_count_greater_0)
    3.32 -
    3.33 -lemma sorted_quicksort: "sorted (quicksort xs)"
    3.34 -  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
    3.35 -
    3.36 -theorem quicksort_sort [code_unfold]:
    3.37 -  "sort = quicksort"
    3.38 -  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
    3.39 -
    3.40 -end
    3.41 -
    3.42 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/Quicksort.thy	Wed Nov 03 12:20:33 2010 +0100
     4.3 @@ -0,0 +1,39 @@
     4.4 +(*  Author:     Tobias Nipkow
     4.5 +    Copyright   1994 TU Muenchen
     4.6 +*)
     4.7 +
     4.8 +header {* Quicksort with function package *}
     4.9 +
    4.10 +theory Quicksort
    4.11 +imports Main Multiset
    4.12 +begin
    4.13 +
    4.14 +context linorder
    4.15 +begin
    4.16 +
    4.17 +fun quicksort :: "'a list \<Rightarrow> 'a list" where
    4.18 +  "quicksort []     = []"
    4.19 +| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    4.20 +
    4.21 +lemma [code]:
    4.22 +  "quicksort []     = []"
    4.23 +  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    4.24 +  by (simp_all add: not_le)
    4.25 +
    4.26 +lemma quicksort_permutes [simp]:
    4.27 +  "multiset_of (quicksort xs) = multiset_of xs"
    4.28 +  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
    4.29 +
    4.30 +lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    4.31 +  by (simp add: set_count_greater_0)
    4.32 +
    4.33 +lemma sorted_quicksort: "sorted (quicksort xs)"
    4.34 +  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
    4.35 +
    4.36 +theorem sort_quicksort:
    4.37 +  "sort = quicksort"
    4.38 +  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
    4.39 +
    4.40 +end
    4.41 +
    4.42 +end
     5.1 --- a/src/HOL/ex/ROOT.ML	Wed Nov 03 12:20:33 2010 +0100
     5.2 +++ b/src/HOL/ex/ROOT.ML	Wed Nov 03 12:20:33 2010 +0100
     5.3 @@ -66,7 +66,8 @@
     5.4    "Execute_Choice",
     5.5    "Summation",
     5.6    "Gauge_Integration",
     5.7 -  "Dedekind_Real"
     5.8 +  "Dedekind_Real",
     5.9 +  "Quicksort"
    5.10  ];
    5.11  
    5.12  HTML.with_charset "utf-8" (no_document use_thys)