--- a/src/HOL/IsaMakefile Tue Sep 18 05:42:46 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 18 06:21:40 2007 +0200
@@ -212,7 +212,7 @@
Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
Library/NatPair.thy \
Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
- Library/Nat_Infinity.thy Library/Word.thy \
+ Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
Library/README.html Library/Continuity.thy \
Library/Nested_Environment.thy Library/Zorn.thy\
Library/Library/ROOT.ML Library/Library/document/root.tex \
@@ -248,7 +248,7 @@
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
- Induct/Common_Patterns.thy Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
+ Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\
Induct/ROOT.ML \
@@ -659,12 +659,12 @@
ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
- ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
+ ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
ex/NatSum.thy ex/NBE.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
- ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
+ ex/Puzzle.thy ex/Quickcheck_Examples.thy \
ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
--- a/src/HOL/List.thy Tue Sep 18 05:42:46 2007 +0200
+++ b/src/HOL/List.thy Tue Sep 18 06:21:40 2007 +0200
@@ -8,8 +8,6 @@
theory List
imports PreList
uses "Tools/string_syntax.ML"
- ("Tools/function_package/lexicographic_order.ML")
- ("Tools/function_package/fundef_datatype.ML")
begin
datatype 'a list =
@@ -220,6 +218,23 @@
"splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
-- {*Warning: simpset does not contain the second eqn but a derived one. *}
+text{* The following simple sort functions are intended for proofs,
+not for efficient implementations. *}
+
+fun (in linorder) sorted :: "'a list \<Rightarrow> bool" where
+"sorted [] \<longleftrightarrow> True" |
+"sorted [x] \<longleftrightarrow> True" |
+"sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
+
+fun (in linorder) insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort x [] = [x]" |
+"insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
+
+fun (in linorder) sort :: "'a list \<Rightarrow> 'a list" where
+"sort [] = []" |
+"sort (x#xs) = insort x (sort xs)"
+
+
subsubsection {* List comprehension *}
text{* Input syntax for Haskell-like list comprehension notation.
@@ -2475,6 +2490,44 @@
apply auto
done
+
+subsection {*Sorting*}
+
+context linorder
+begin
+
+lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x \<^loc><= y))"
+apply(induct xs arbitrary: x) apply simp
+by simp (blast intro: order_trans)
+
+lemma sorted_append:
+ "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<^loc>\<le>y))"
+by (induct xs) (auto simp add:sorted_Cons)
+
+lemma set_insort: "set(insort x xs) = insert x (set xs)"
+by (induct xs) auto
+
+lemma set_sort: "set(sort xs) = set xs"
+by (induct xs) (simp_all add:set_insort)
+
+lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
+by(induct xs)(auto simp:set_insort)
+
+lemma distinct_sort: "distinct (sort xs) = distinct xs"
+by(induct xs)(simp_all add:distinct_insort set_sort)
+
+lemma sorted_insort: "sorted (insort x xs) = sorted xs"
+apply (induct xs)
+ apply(auto simp:sorted_Cons set_insort not_le less_imp_le)
+apply(blast intro:order_trans)
+done
+
+theorem sorted_sort[simp]: "sorted (sort xs)"
+by (induct xs) (auto simp:sorted_insort)
+
+end
+
+
subsubsection {* @{text lists}: the list-forming operator over sets *}
inductive_set
--- a/src/HOL/PreList.thy Tue Sep 18 05:42:46 2007 +0200
+++ b/src/HOL/PreList.thy Tue Sep 18 06:21:40 2007 +0200
@@ -8,6 +8,8 @@
theory PreList
imports Presburger Relation_Power SAT Recdef Extraction Record
+uses "Tools/function_package/lexicographic_order.ML"
+ "Tools/function_package/fundef_datatype.ML"
begin
text {*
@@ -15,5 +17,9 @@
theory ToyList in the documentation.
*}
+(* The lexicographic_order method and the "fun" command *)
+setup LexicographicOrder.setup
+setup FundefDatatype.setup
+
end