# HG changeset patch # User haftmann # Date 1288860856 -3600 # Node ID d7dfec07806a6c9ab919032515002e6ce28c285f # Parent df25b51af0134b259a27255793d7ba534cb116e4# Parent 2f44afc0fff30887141cf43e85efaca6207b84f0 merged diff -r df25b51af013 -r d7dfec07806a NEWS --- a/NEWS Wed Nov 03 23:01:30 2010 +0100 +++ b/NEWS Thu Nov 04 09:54:16 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, diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/Adaptation.thy Thu Nov 04 09:54:16 2010 +0100 @@ -2,7 +2,8 @@ imports Setup begin -setup %invisible {* Code_Target.extend_target ("\", ("SML", K I)) *} +setup %invisible {* Code_Target.extend_target ("\", ("SML", K I)) + #> Code_Target.extend_target ("\", ("Haskell", K I)) *} section {* Adaptation to target languages \label{sec:adaptation} *} @@ -235,7 +236,7 @@ @{command_def "code_reserved"} command: *} -code_reserved %quote "\" bool true false andalso +code_reserved %quote "\" bool true false andalso text {* \noindent Next, we try to map HOL pairs to SML pairs, using the diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/Evaluation.thy --- a/doc-src/Codegen/Thy/Evaluation.thy Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/Evaluation.thy Thu Nov 04 09:54:16 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"}. diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/Further.thy Thu Nov 04 09:54:16 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. *} diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/Refinement.thy --- a/doc-src/Codegen/Thy/Refinement.thy Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/Refinement.thy Thu Nov 04 09:54:16 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: *} diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu Nov 04 09:54:16 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}% % diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/document/Evaluation.tex --- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Thu Nov 04 09:54:16 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}. diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Further.tex Thu Nov 04 09:54:16 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% % diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Thu Nov 04 09:54:16 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% diff -r df25b51af013 -r d7dfec07806a doc-src/Codegen/style.sty --- a/doc-src/Codegen/style.sty Wed Nov 03 23:01:30 2010 +0100 +++ b/doc-src/Codegen/style.sty Thu Nov 04 09:54:16 2010 +0100 @@ -45,6 +45,7 @@ %% a trick \newcommand{\isasymSML}{SML} +\newcommand{\isasymSMLdummy}{SML} %% presentation \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} diff -r df25b51af013 -r d7dfec07806a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Nov 03 23:01:30 2010 +0100 +++ b/src/HOL/IsaMakefile Thu Nov 04 09:54:16 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 df25b51af013 -r d7dfec07806a src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Nov 03 23:01:30 2010 +0100 +++ b/src/HOL/Library/Library.thy Thu Nov 04 09:54:16 2010 +0100 @@ -45,7 +45,6 @@ Polynomial Preorder Product_Vector - Quicksort Quotient_List Quotient_Option Quotient_Product diff -r df25b51af013 -r d7dfec07806a src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Nov 03 23:01:30 2010 +0100 +++ b/src/HOL/Library/Multiset.thy Thu Nov 04 09:54:16 2010 +0100 @@ -901,30 +901,27 @@ next fix l assume "l \ set ?rhs" - have *: "\x P. P (f x) \ f l = f x \ P (f l) \ f l = f x" by auto - have **: "\x. f l = f x \ f x = f l" by auto + let ?pivot = "f (xs ! (length xs div 2))" + have *: "\x. f l = f x \ f x = f l" by auto have "[x \ sort_key f xs . f x = f l] = [x \ xs. f x = f l]" unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) - with ** have [simp]: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp - let ?pivot = "f (xs ! (length xs div 2))" + with * have **: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp + have "\x P. P (f x) ?pivot \ f l = f x \ P (f l) ?pivot \ f l = f x" by auto + then have "\P. [x \ sort_key f xs . P (f x) ?pivot \ f l = f x] = + [x \ sort_key f xs. P (f l) ?pivot \ f l = f x]" by simp + note *** = this [of "op <"] this [of "op >"] this [of "op ="] show "[x \ ?rhs. f l = f x] = [x \ ?lhs. f l = f x]" proof (cases "f l" ?pivot rule: linorder_cases) case less then moreover have "f l \ ?pivot" and "\ 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 \ ?pivot" and "\ 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\xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs") using sort_key_by_quicksort [of "\x. x", symmetric] by simp +text {* A stable parametrized quicksort *} + +definition part :: "('b \ 'a) \ 'a \ 'b list \ 'b list \ 'b list \ 'b list" where + "part f pivot xs = ([x \ xs. f x < pivot], [x \ xs. f x = pivot], [x \ 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 [] \ [] + | [x] \ xs + | [x, y] \ (if f x \ f y then xs else [y, x]) + | _ \ (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) \ multiset_of xs" by (induct xs) (auto intro: order_trans) diff -r df25b51af013 -r d7dfec07806a src/HOL/Library/Quicksort.thy --- a/src/HOL/Library/Quicksort.thy Wed Nov 03 23:01:30 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 \ 'a list" where - "quicksort [] = []" -| "quicksort (x#xs) = quicksort [y\xs. \ x\y] @ [x] @ quicksort [y\xs. x\y]" - -lemma [code]: - "quicksort [] = []" - "quicksort (x#xs) = quicksort [y\xs. yxs. x\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 df25b51af013 -r d7dfec07806a src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Wed Nov 03 23:01:30 2010 +0100 +++ b/src/HOL/Tools/primrec.ML Thu Nov 04 09:54:16 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) => diff -r df25b51af013 -r d7dfec07806a src/HOL/ex/Quicksort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Quicksort.thy Thu Nov 04 09:54:16 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 \ 'a list" where + "quicksort [] = []" +| "quicksort (x#xs) = quicksort [y\xs. \ x\y] @ [x] @ quicksort [y\xs. x\y]" + +lemma [code]: + "quicksort [] = []" + "quicksort (x#xs) = quicksort [y\xs. yxs. x\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 df25b51af013 -r d7dfec07806a src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Nov 03 23:01:30 2010 +0100 +++ b/src/HOL/ex/ROOT.ML Thu Nov 04 09:54:16 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)