Added function package to PreList
authornipkow
Tue Sep 18 05:42:46 2007 +0200 (2007-09-18)
changeset 2461517dbd993293d
parent 24614 a4b2eb0dd673
child 24616 fac3dd4ade83
Added function package to PreList
Added sorted/sort to List
Moved qsort from ex to Library
src/HOL/Library/Library.thy
src/HOL/Library/Quicksort.thy
src/HOL/ex/InSort.thy
src/HOL/ex/Qsort.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/Library/Library.thy	Mon Sep 17 16:36:45 2007 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Tue Sep 18 05:42:46 2007 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    Pretty_Char_chr
     1.5    Pretty_Int
     1.6    Primes
     1.7 +  Quicksort
     1.8    Quotient
     1.9    Ramsey
    1.10    State_Monad
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Quicksort.thy	Tue Sep 18 05:42:46 2007 +0200
     2.3 @@ -0,0 +1,44 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Tobias Nipkow
     2.6 +    Copyright   1994 TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header{*Quicksort*}
    2.10 +
    2.11 +theory Quicksort
    2.12 +imports Multiset
    2.13 +begin
    2.14 +
    2.15 +context linorder
    2.16 +begin
    2.17 +
    2.18 +function quicksort :: "'a list \<Rightarrow> 'a list" where
    2.19 +"quicksort []     = []" |
    2.20 +"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<^loc>\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<^loc>\<le>y])"
    2.21 +by pat_completeness auto
    2.22 +
    2.23 +termination
    2.24 +by (relation "measure size")
    2.25 +   (auto simp: length_filter_le[THEN order_class.le_less_trans])
    2.26 +
    2.27 +end
    2.28 +context linorder
    2.29 +begin
    2.30 +
    2.31 +lemma quicksort_permutes [simp]:
    2.32 +  "multiset_of (quicksort xs) = multiset_of xs"
    2.33 +by (induct xs rule: quicksort.induct) (auto simp: union_ac)
    2.34 +
    2.35 +lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
    2.36 +by(simp add: set_count_greater_0)
    2.37 +
    2.38 +lemma sorted_quicksort: "sorted(quicksort xs)"
    2.39 +apply (induct xs rule: quicksort.induct)
    2.40 + apply simp
    2.41 +apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
    2.42 +apply (metis leD le_cases le_less_trans)
    2.43 +done
    2.44 +
    2.45 +end
    2.46 +
    2.47 +end
     3.1 --- a/src/HOL/ex/InSort.thy	Mon Sep 17 16:36:45 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,50 +0,0 @@
     3.4 -(*  Title:      HOL/ex/insort.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -    Copyright   1994 TU Muenchen
     3.8 -*)
     3.9 -
    3.10 -header{*Insertion Sort*}
    3.11 -
    3.12 -theory InSort
    3.13 -imports Sorting
    3.14 -begin
    3.15 -
    3.16 -consts
    3.17 -  ins    :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.18 -  insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.19 -
    3.20 -primrec
    3.21 -  "ins le x [] = [x]"
    3.22 -  "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"
    3.23 -
    3.24 -primrec
    3.25 -  "insort le [] = []"
    3.26 -  "insort le (x#xs) = ins le x (insort le xs)"
    3.27 -
    3.28 -
    3.29 -lemma multiset_ins[simp]:
    3.30 - "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
    3.31 -  by (induct xs) (auto simp: union_ac)
    3.32 -
    3.33 -theorem insort_permutes[simp]:
    3.34 - "\<And>x. multiset_of (insort le xs) = multiset_of xs"
    3.35 -  by (induct "xs") auto
    3.36 -
    3.37 -lemma set_ins [simp]: "set(ins le x xs) = insert x (set xs)"
    3.38 -  by (simp add: set_count_greater_0) fast
    3.39 -
    3.40 -lemma sorted_ins[simp]:
    3.41 - "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
    3.42 -apply (induct xs)
    3.43 -apply simp_all
    3.44 -apply (unfold Sorting.total_def Sorting.transf_def)
    3.45 -apply blast
    3.46 -done
    3.47 -
    3.48 -theorem sorted_insort:
    3.49 - "[| total(le); transf(le) |] ==>  sorted le (insort le xs)"
    3.50 -by (induct xs) auto
    3.51 -
    3.52 -end
    3.53 -
     4.1 --- a/src/HOL/ex/Qsort.thy	Mon Sep 17 16:36:45 2007 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,59 +0,0 @@
     4.4 -(*  Title:      HOL/ex/Qsort.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow
     4.7 -    Copyright   1994 TU Muenchen
     4.8 -*)
     4.9 -
    4.10 -header{*Quicksort*}
    4.11 -
    4.12 -theory Qsort
    4.13 -imports Sorting
    4.14 -begin
    4.15 -
    4.16 -subsection{*Version 1: higher-order*}
    4.17 -
    4.18 -consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"
    4.19 -
    4.20 -recdef qsort "measure (size o snd)"
    4.21 -    "qsort(le, [])   = []"
    4.22 -    "qsort(le, x#xs) = qsort(le, [y\<leftarrow>xs . ~ le x y]) @ [x] @
    4.23 -		       qsort(le, [y\<leftarrow>xs . le x y])"
    4.24 -(hints recdef_simp: length_filter_le[THEN le_less_trans])
    4.25 -
    4.26 -lemma qsort_permutes [simp]:
    4.27 -     "multiset_of (qsort(le,xs)) = multiset_of xs"
    4.28 -by (induct le xs rule: qsort.induct) (auto simp: union_ac)
    4.29 -
    4.30 -lemma set_qsort [simp]: "set (qsort(le,xs)) = set xs";
    4.31 -by(simp add: set_count_greater_0)
    4.32 -
    4.33 -lemma sorted_qsort:
    4.34 -     "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
    4.35 -apply (induct le xs rule: qsort.induct)
    4.36 - apply simp
    4.37 -apply simp
    4.38 -apply(unfold Sorting.total_def Sorting.transf_def)
    4.39 -apply blast
    4.40 -done
    4.41 -
    4.42 -
    4.43 -subsection{*Version 2:type classes*}
    4.44 -
    4.45 -consts quickSort :: "('a::linorder) list => 'a list"
    4.46 -
    4.47 -recdef quickSort "measure size"
    4.48 -    "quickSort []   = []"
    4.49 -    "quickSort (x#l) = quickSort [y\<leftarrow>l. ~ x\<le>y] @ [x] @ quickSort [y\<leftarrow>l. x\<le>y]"
    4.50 -(hints recdef_simp: length_filter_le[THEN le_less_trans])
    4.51 -
    4.52 -lemma quickSort_permutes[simp]:
    4.53 - "multiset_of (quickSort xs) = multiset_of xs"
    4.54 -by (induct xs rule: quickSort.induct) (auto simp: union_ac)
    4.55 -
    4.56 -lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
    4.57 -by(simp add: set_count_greater_0)
    4.58 -
    4.59 -theorem sorted_quickSort: "sorted (op \<le>) (quickSort xs)"
    4.60 -by (induct xs rule: quickSort.induct, auto)
    4.61 -
    4.62 -end
     5.1 --- a/src/HOL/ex/ROOT.ML	Mon Sep 17 16:36:45 2007 +0200
     5.2 +++ b/src/HOL/ex/ROOT.ML	Tue Sep 18 05:42:46 2007 +0200
     5.3 @@ -32,8 +32,6 @@
     5.4    "CTL",
     5.5    "Arith_Examples",
     5.6    "BT",
     5.7 -  "InSort",
     5.8 -  "Qsort",
     5.9    "MergeSort",
    5.10    "Puzzle",
    5.11    "Lagrange",