--- a/NEWS Thu Nov 04 09:53:23 2010 +0100
+++ b/NEWS Thu Nov 04 13:37:11 2010 +0100
@@ -82,6 +82,8 @@
*** HOL ***
+* Theory Multiset provides stable quicksort implementation of sort_key.
+
* Quickcheck now has a configurable time limit which is set to 30 seconds
by default. This can be changed by adding [timeout = n] to the quickcheck
command. The time limit for auto quickcheck is still set independently,
--- a/doc-src/Codegen/Thy/Adaptation.thy Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy Thu Nov 04 13:37:11 2010 +0100
@@ -2,7 +2,8 @@
imports Setup
begin
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I)) *}
+setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
+ #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
section {* Adaptation to target languages \label{sec:adaptation} *}
@@ -235,7 +236,7 @@
@{command_def "code_reserved"} command:
*}
-code_reserved %quote "\<SML>" bool true false andalso
+code_reserved %quote "\<SMLdummy>" bool true false andalso
text {*
\noindent Next, we try to map HOL pairs to SML pairs, using the
--- a/doc-src/Codegen/Thy/Evaluation.thy Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/Evaluation.thy Thu Nov 04 13:37:11 2010 +0100
@@ -18,7 +18,7 @@
subsection {* Evaluation techniques *}
text {*
- The existing infrastructure provides a rich palett of evaluation
+ The existing infrastructure provides a rich palette of evaluation
techniques, each comprising different aspects:
\begin{description}
@@ -135,7 +135,7 @@
"t'"}.
\item Evaluation of @{term t} terminates which en exception
- indicating a pattern match failure or a not-implemented
+ indicating a pattern match failure or a non-implemented
function. As sketched in \secref{sec:partiality}, this can be
interpreted as partiality.
@@ -148,8 +148,8 @@
Exceptions of the third kind are propagated to the user.
By default return values of plain evaluation are optional, yielding
- @{text "SOME t'"} in the first case, @{text "NONE"} and in the
- second propagating the exception in the third case. A strict
+ @{text "SOME t'"} in the first case, @{text "NONE"} in the
+ second, and propagating the exception in the third case. A strict
variant of plain evaluation either yields @{text "t'"} or propagates
any exception, a liberal variant caputures any exception in a result
of type @{text "Exn.result"}.
--- a/doc-src/Codegen/Thy/Further.thy Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Thu Nov 04 13:37:11 2010 +0100
@@ -124,7 +124,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session @{text Imperative_HOL}.
+ is available in session @{text Imperative_HOL}, together with a short
+ primer document.
*}
--- a/doc-src/Codegen/Thy/Refinement.thy Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/Refinement.thy Thu Nov 04 13:37:11 2010 +0100
@@ -17,7 +17,7 @@
text {*
Program refinement works by choosing appropriate code equations
- explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
numbers:
*}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu Nov 04 13:37:11 2010 +0100
@@ -26,7 +26,8 @@
%
\isataginvisible
\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharhash}{\isachargreater}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSMLdummy}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}Haskell{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -420,7 +421,7 @@
%
\isatagquote
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
+\ {\isachardoublequoteopen}{\isasymSMLdummy}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
\endisatagquote
{\isafoldquote}%
%
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Thu Nov 04 13:37:11 2010 +0100
@@ -38,7 +38,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The existing infrastructure provides a rich palett of evaluation
+The existing infrastructure provides a rich palette of evaluation
techniques, each comprising different aspects:
\begin{description}
@@ -188,7 +188,7 @@
\item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}.
\item Evaluation of \isa{t} terminates which en exception
- indicating a pattern match failure or a not-implemented
+ indicating a pattern match failure or a non-implemented
function. As sketched in \secref{sec:partiality}, this can be
interpreted as partiality.
@@ -200,8 +200,8 @@
Exceptions of the third kind are propagated to the user.
By default return values of plain evaluation are optional, yielding
- \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} and in the
- second propagating the exception in the third case. A strict
+ \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} in the
+ second, and propagating the exception in the third case. A strict
variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates
any exception, a liberal variant caputures any exception in a result
of type \isa{Exn{\isachardot}result}.
--- a/doc-src/Codegen/Thy/document/Further.tex Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Thu Nov 04 13:37:11 2010 +0100
@@ -240,7 +240,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session \isa{Imperative{\isacharunderscore}HOL}.%
+ is available in session \isa{Imperative{\isacharunderscore}HOL}, together with a short
+ primer document.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Thu Nov 04 13:37:11 2010 +0100
@@ -37,7 +37,7 @@
%
\begin{isamarkuptext}%
Program refinement works by choosing appropriate code equations
- explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/style.sty Thu Nov 04 09:53:23 2010 +0100
+++ b/doc-src/Codegen/style.sty Thu Nov 04 13:37:11 2010 +0100
@@ -45,6 +45,7 @@
%% a trick
\newcommand{\isasymSML}{SML}
+\newcommand{\isasymSMLdummy}{SML}
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
--- a/src/HOL/IsaMakefile Thu Nov 04 09:53:23 2010 +0100
+++ b/src/HOL/IsaMakefile Thu Nov 04 13:37:11 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
--- a/src/HOL/Library/Library.thy Thu Nov 04 09:53:23 2010 +0100
+++ b/src/HOL/Library/Library.thy Thu Nov 04 13:37:11 2010 +0100
@@ -45,7 +45,6 @@
Polynomial
Preorder
Product_Vector
- Quicksort
Quotient_List
Quotient_Option
Quotient_Product
--- a/src/HOL/Library/Multiset.thy Thu Nov 04 09:53:23 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Nov 04 13:37:11 2010 +0100
@@ -901,30 +901,27 @@
next
fix l
assume "l \<in> set ?rhs"
- have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto
- have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
+ let ?pivot = "f (xs ! (length xs div 2))"
+ have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
- with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
- let ?pivot = "f (xs ! (length xs div 2))"
+ with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
+ have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto
+ then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
+ [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
+ note *** = this [of "op <"] this [of "op >"] this [of "op ="]
show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
ultimately show ?thesis
- apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply simp
- apply (subst *) apply simp
- done
+ by (simp add: filter_sort [symmetric] ** ***)
next
case equal then show ?thesis
- by (auto simp add: ** less_le)
+ by (simp add: * less_le)
next
case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
ultimately show ?thesis
- apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply simp
- apply (subst *) apply simp
- done
+ by (simp add: filter_sort [symmetric] ** ***)
qed
qed
@@ -934,8 +931,48 @@
@ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
+text {* A stable parametrized quicksort *}
+
+definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
+ "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
+
+lemma part_code [code]:
+ "part f pivot [] = ([], [], [])"
+ "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in
+ if x' < pivot then (x # lts, eqs, gts)
+ else if x' > pivot then (lts, eqs, x # gts)
+ else (lts, x # eqs, gts))"
+ by (auto simp add: part_def Let_def split_def)
+
+lemma sort_key_by_quicksort_code [code]:
+ "sort_key f xs = (case xs of [] \<Rightarrow> []
+ | [x] \<Rightarrow> xs
+ | [x, y] \<Rightarrow> (if f x \<le> f y then xs else [y, x])
+ | _ \<Rightarrow> (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
+ in sort_key f lts @ eqs @ sort_key f gts))"
+proof (cases xs)
+ case Nil then show ?thesis by simp
+next
+ case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+ case Nil with hyps show ?thesis by simp
+ next
+ case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+ case Nil with hyps show ?thesis by auto
+ next
+ case Cons
+ from sort_key_by_quicksort [of f xs]
+ have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
+ in sort_key f lts @ eqs @ sort_key f gts)"
+ by (simp only: split_def Let_def part_def fst_conv snd_conv)
+ with hyps Cons show ?thesis by (simp only: list.cases)
+ qed
+ qed
+qed
+
end
+hide_const (open) part
+
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
by (induct xs) (auto intro: order_trans)
--- a/src/HOL/Library/Quicksort.thy Thu Nov 04 09:53:23 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
--- a/src/HOL/Tools/primrec.ML Thu Nov 04 09:53:23 2010 +0100
+++ b/src/HOL/Tools/primrec.ML Thu Nov 04 13:37:11 2010 +0100
@@ -31,8 +31,6 @@
fun primrec_error msg = raise PrimrecError (msg, NONE);
fun primrec_error_eqn msg eqn = raise PrimrecError (msg, SOME eqn);
-fun message s = if ! Toplevel.debug then tracing s else ();
-
(* preprocessing of equations *)
@@ -251,7 +249,6 @@
if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
val rewrites = rec_rewrites' @ map (snd o snd) defs;
fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
- val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
in map (fn eq => Goal.prove lthy frees [] eq tac) eqs end;
in ((prefix, (fs, defs)), prove) end
handle PrimrecError (msg, some_eqn) =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Quicksort.thy Thu Nov 04 13:37:11 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
--- a/src/HOL/ex/ROOT.ML Thu Nov 04 09:53:23 2010 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Nov 04 13:37:11 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)