# HG changeset patch
# User nipkow
# Date 1190089300 -7200
# Node ID fac3dd4ade836b156cdae3e740a42592c57321fb
# Parent  17dbd993293d3723dbaa407268e959291c90397d
sorting

diff -r 17dbd993293d -r fac3dd4ade83 src/HOL/IsaMakefile
--- 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 \
diff -r 17dbd993293d -r fac3dd4ade83 src/HOL/List.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
diff -r 17dbd993293d -r fac3dd4ade83 src/HOL/PreList.thy
--- 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