--- a/src/HOL/ex/InSort.thy Fri Apr 22 15:10:42 2005 +0200
+++ b/src/HOL/ex/InSort.thy Fri Apr 22 17:32:03 2005 +0200
@@ -2,14 +2,16 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
-
-Insertion sort
*)
-theory InSort = Sorting:
+header{*Insertion Sort*}
+
+theory InSort
+imports Sorting
+begin
consts
- ins :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ ins :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
@@ -25,11 +27,11 @@
"\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
by (induct xs) (auto simp: union_ac)
-lemma insort_permutes[simp]:
+theorem insort_permutes[simp]:
"\<And>x. multiset_of (insort le xs) = multiset_of xs"
by (induct "xs") auto
-lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)"
+lemma set_ins [simp]: "set(ins le x xs) = insert x (set xs)"
by (simp add: set_count_greater_0) fast
lemma sorted_ins[simp]:
@@ -40,7 +42,7 @@
apply blast
done
-lemma sorted_insort:
+theorem sorted_insort:
"[| total(le); transf(le) |] ==> sorted le (insort le xs)"
by (induct xs) auto
--- a/src/HOL/ex/MergeSort.thy Fri Apr 22 15:10:42 2005 +0200
+++ b/src/HOL/ex/MergeSort.thy Fri Apr 22 17:32:03 2005 +0200
@@ -2,22 +2,26 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TU Muenchen
-
-Merge sort
*)
-theory MergeSort = Sorting:
+header{*Merge Sort*}
+
+theory MergeSort
+imports Sorting
+begin
consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
recdef merge "measure(%(xs,ys). size xs + size ys)"
-"merge(x#xs,y#ys) =
- (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
-"merge(xs,[]) = xs"
-"merge([],ys) = ys"
+ "merge(x#xs, y#ys) =
+ (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
+
+ "merge(xs,[]) = xs"
+
+ "merge([],ys) = ys"
lemma multiset_of_merge[simp]:
- "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
+ "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
apply(induct xs ys rule: merge.induct)
apply (auto simp: union_ac)
done
@@ -28,27 +32,25 @@
done
lemma sorted_merge[simp]:
- "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
+ "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
apply(induct xs ys rule: merge.induct)
-apply(simp_all add:ball_Un linorder_not_le order_less_le)
+apply(simp_all add: ball_Un linorder_not_le order_less_le)
apply(blast intro: order_trans)
done
consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
recdef msort "measure size"
-"msort [] = []"
-"msort [x] = [x]"
-"msort xs = merge(msort(take (size xs div 2) xs),
- msort(drop (size xs div 2) xs))"
+ "msort [] = []"
+ "msort [x] = [x]"
+ "msort xs = merge(msort(take (size xs div 2) xs),
+ msort(drop (size xs div 2) xs))"
-lemma sorted_msort: "sorted op <= (msort xs)"
+theorem sorted_msort: "sorted (op \<le>) (msort xs)"
by (induct xs rule: msort.induct) simp_all
-lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
+theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
apply (induct xs rule: msort.induct)
- apply simp
- apply simp
-apply simp
+ apply simp_all
apply (subst union_commute)
apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
apply (simp add: union_ac)
--- a/src/HOL/ex/Qsort.thy Fri Apr 22 15:10:42 2005 +0200
+++ b/src/HOL/ex/Qsort.thy Fri Apr 22 17:32:03 2005 +0200
@@ -2,31 +2,33 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
-
-Quicksort
*)
-theory Qsort = Sorting:
+header{*Quicksort*}
-(*Version one: higher-order*)
+theory Qsort
+imports Sorting
+begin
+
+subsection{*Version 1: higher-order*}
+
consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"
recdef qsort "measure (size o snd)"
-"qsort(le, []) = []"
-"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
- qsort(le, [y:xs . le x y])"
+ "qsort(le, []) = []"
+ "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
+ qsort(le, [y:xs . le x y])"
(hints recdef_simp: length_filter_le[THEN le_less_trans])
-lemma qsort_permutes[simp]:
- "multiset_of (qsort(le,xs)) = multiset_of xs"
+lemma qsort_permutes [simp]:
+ "multiset_of (qsort(le,xs)) = multiset_of xs"
by (induct le xs rule: qsort.induct) (auto simp: union_ac)
-(*Also provable by induction*)
-lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
+lemma set_qsort [simp]: "set (qsort(le,xs)) = set xs";
by(simp add: set_count_greater_0)
lemma sorted_qsort:
- "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
+ "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
apply (induct le xs rule: qsort.induct)
apply simp
apply simp
@@ -35,28 +37,23 @@
done
-(*Version two: type classes*)
+subsection{*Version 2:type classes*}
consts quickSort :: "('a::linorder) list => 'a list"
recdef quickSort "measure size"
-"quickSort [] = []"
-"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
+ "quickSort [] = []"
+ "quickSort (x#l) = quickSort [y:l. ~ x\<le>y] @ [x] @ quickSort [y:l. x\<le>y]"
(hints recdef_simp: length_filter_le[THEN le_less_trans])
lemma quickSort_permutes[simp]:
"multiset_of (quickSort xs) = multiset_of xs"
by (induct xs rule: quickSort.induct) (auto simp: union_ac)
-(*Also provable by induction*)
lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
by(simp add: set_count_greater_0)
-lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
-apply (induct xs rule: quickSort.induct)
- apply simp
-apply simp
-apply(blast intro: linorder_linear[THEN disjE] order_trans)
-done
+theorem sorted_quickSort: "sorted (op \<le>) (quickSort xs)"
+by (induct xs rule: quickSort.induct, auto)
end
--- a/src/HOL/ex/Sorting.thy Fri Apr 22 15:10:42 2005 +0200
+++ b/src/HOL/ex/Sorting.thy Fri Apr 22 17:32:03 2005 +0200
@@ -2,11 +2,13 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1994 TU Muenchen
-
-Specification of sorting
*)
-theory Sorting = Main + Multiset:
+header{*Sorting: Basic Theory*}
+
+theory Sorting
+imports Main Multiset
+begin
consts
sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -19,22 +21,21 @@
primrec
"sorted le [] = True"
- "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
+ "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
constdefs
total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
- "total r == (ALL x y. r x y | r y x)"
+ "total r == (\<forall>x y. r x y | r y x)"
transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
- "transf f == (ALL x y z. f x y & f y z --> f x z)"
+ "transf f == (\<forall>x y z. f x y & f y z --> f x z)"
(* Equivalence of two definitions of `sorted' *)
-lemma sorted1_is_sorted:
- "transf(le) ==> sorted1 le xs = sorted le xs";
+lemma sorted1_is_sorted: "transf(le) ==> sorted1 le xs = sorted le xs";
apply(induct xs)
apply simp
apply(simp split: list.split)
@@ -42,9 +43,9 @@
apply(blast)
done
-lemma sorted_append[simp]:
- "sorted le (xs@ys) = (sorted le xs \<and> sorted le ys \<and>
- (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
+lemma sorted_append [simp]:
+ "sorted le (xs@ys) =
+ (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
by (induct xs, auto)
end