# HG changeset patch
# User paulson
# Date 1114183923 -7200
# Node ID 62854cac54104b6c3d9b3f190a6c06a912415eb0
# Parent  d65f461c8672887f1e8f1b0eb1197bc884d88343
tidied

diff -r d65f461c8672 -r 62854cac5410 src/HOL/ex/InSort.thy
--- 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
 
diff -r d65f461c8672 -r 62854cac5410 src/HOL/ex/MergeSort.thy
--- 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)
diff -r d65f461c8672 -r 62854cac5410 src/HOL/ex/Qsort.thy
--- 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
diff -r d65f461c8672 -r 62854cac5410 src/HOL/ex/Sorting.thy
--- 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