tidied
authorpaulson
Fri Apr 22 17:32:03 2005 +0200 (2005-04-22)
changeset 1581562854cac5410
parent 15814 d65f461c8672
child 15816 4575c87dd25b
tidied
src/HOL/ex/InSort.thy
src/HOL/ex/MergeSort.thy
src/HOL/ex/Qsort.thy
src/HOL/ex/Sorting.thy
     1.1 --- a/src/HOL/ex/InSort.thy	Fri Apr 22 15:10:42 2005 +0200
     1.2 +++ b/src/HOL/ex/InSort.thy	Fri Apr 22 17:32:03 2005 +0200
     1.3 @@ -2,14 +2,16 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow
     1.6      Copyright   1994 TU Muenchen
     1.7 -
     1.8 -Insertion sort
     1.9  *)
    1.10  
    1.11 -theory InSort  =  Sorting:
    1.12 +header{*Insertion Sort*}
    1.13 +
    1.14 +theory InSort
    1.15 +imports Sorting
    1.16 +begin
    1.17  
    1.18  consts
    1.19 -  ins :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.20 +  ins    :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.21    insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.22  
    1.23  primrec
    1.24 @@ -25,11 +27,11 @@
    1.25   "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
    1.26    by (induct xs) (auto simp: union_ac)
    1.27  
    1.28 -lemma insort_permutes[simp]:
    1.29 +theorem insort_permutes[simp]:
    1.30   "\<And>x. multiset_of (insort le xs) = multiset_of xs"
    1.31    by (induct "xs") auto
    1.32  
    1.33 -lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)"
    1.34 +lemma set_ins [simp]: "set(ins le x xs) = insert x (set xs)"
    1.35    by (simp add: set_count_greater_0) fast
    1.36  
    1.37  lemma sorted_ins[simp]:
    1.38 @@ -40,7 +42,7 @@
    1.39  apply blast
    1.40  done
    1.41  
    1.42 -lemma sorted_insort:
    1.43 +theorem sorted_insort:
    1.44   "[| total(le); transf(le) |] ==>  sorted le (insort le xs)"
    1.45  by (induct xs) auto
    1.46  
     2.1 --- a/src/HOL/ex/MergeSort.thy	Fri Apr 22 15:10:42 2005 +0200
     2.2 +++ b/src/HOL/ex/MergeSort.thy	Fri Apr 22 17:32:03 2005 +0200
     2.3 @@ -2,22 +2,26 @@
     2.4      ID:         $Id$
     2.5      Author:     Tobias Nipkow
     2.6      Copyright   2002 TU Muenchen
     2.7 -
     2.8 -Merge sort
     2.9  *)
    2.10  
    2.11 -theory MergeSort = Sorting:
    2.12 +header{*Merge Sort*}
    2.13 +
    2.14 +theory MergeSort
    2.15 +imports Sorting
    2.16 +begin
    2.17  
    2.18  consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
    2.19  
    2.20  recdef merge "measure(%(xs,ys). size xs + size ys)"
    2.21 -"merge(x#xs,y#ys) =
    2.22 - (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
    2.23 -"merge(xs,[]) = xs"
    2.24 -"merge([],ys) = ys"
    2.25 +    "merge(x#xs, y#ys) =
    2.26 +         (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
    2.27 +
    2.28 +    "merge(xs,[]) = xs"
    2.29 +
    2.30 +    "merge([],ys) = ys"
    2.31  
    2.32  lemma multiset_of_merge[simp]:
    2.33 - "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
    2.34 +     "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
    2.35  apply(induct xs ys rule: merge.induct)
    2.36  apply (auto simp: union_ac)
    2.37  done
    2.38 @@ -28,27 +32,25 @@
    2.39  done
    2.40  
    2.41  lemma sorted_merge[simp]:
    2.42 - "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
    2.43 +     "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
    2.44  apply(induct xs ys rule: merge.induct)
    2.45 -apply(simp_all add:ball_Un linorder_not_le order_less_le)
    2.46 +apply(simp_all add: ball_Un linorder_not_le order_less_le)
    2.47  apply(blast intro: order_trans)
    2.48  done
    2.49  
    2.50  consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
    2.51  recdef msort "measure size"
    2.52 -"msort [] = []"
    2.53 -"msort [x] = [x]"
    2.54 -"msort xs = merge(msort(take (size xs div 2) xs),
    2.55 -                  msort(drop (size xs div 2) xs))"
    2.56 +    "msort [] = []"
    2.57 +    "msort [x] = [x]"
    2.58 +    "msort xs = merge(msort(take (size xs div 2) xs),
    2.59 +		      msort(drop (size xs div 2) xs))"
    2.60  
    2.61 -lemma sorted_msort: "sorted op <= (msort xs)"
    2.62 +theorem sorted_msort: "sorted (op \<le>) (msort xs)"
    2.63  by (induct xs rule: msort.induct) simp_all
    2.64  
    2.65 -lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    2.66 +theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    2.67  apply (induct xs rule: msort.induct)
    2.68 -  apply simp
    2.69 - apply simp
    2.70 -apply simp
    2.71 +  apply simp_all
    2.72  apply (subst union_commute)
    2.73  apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
    2.74  apply (simp add: union_ac)
     3.1 --- a/src/HOL/ex/Qsort.thy	Fri Apr 22 15:10:42 2005 +0200
     3.2 +++ b/src/HOL/ex/Qsort.thy	Fri Apr 22 17:32:03 2005 +0200
     3.3 @@ -2,31 +2,33 @@
     3.4      ID:         $Id$
     3.5      Author:     Tobias Nipkow
     3.6      Copyright   1994 TU Muenchen
     3.7 -
     3.8 -Quicksort
     3.9  *)
    3.10  
    3.11 -theory Qsort = Sorting:
    3.12 +header{*Quicksort*}
    3.13  
    3.14 -(*Version one: higher-order*)
    3.15 +theory Qsort
    3.16 +imports Sorting
    3.17 +begin
    3.18 +
    3.19 +subsection{*Version 1: higher-order*}
    3.20 +
    3.21  consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"
    3.22  
    3.23  recdef qsort "measure (size o snd)"
    3.24 -"qsort(le, [])   = []"
    3.25 -"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
    3.26 -                   qsort(le, [y:xs . le x y])"
    3.27 +    "qsort(le, [])   = []"
    3.28 +    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
    3.29 +		       qsort(le, [y:xs . le x y])"
    3.30  (hints recdef_simp: length_filter_le[THEN le_less_trans])
    3.31  
    3.32 -lemma qsort_permutes[simp]:
    3.33 - "multiset_of (qsort(le,xs)) = multiset_of xs"
    3.34 +lemma qsort_permutes [simp]:
    3.35 +     "multiset_of (qsort(le,xs)) = multiset_of xs"
    3.36  by (induct le xs rule: qsort.induct) (auto simp: union_ac)
    3.37  
    3.38 -(*Also provable by induction*)
    3.39 -lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
    3.40 +lemma set_qsort [simp]: "set (qsort(le,xs)) = set xs";
    3.41  by(simp add: set_count_greater_0)
    3.42  
    3.43  lemma sorted_qsort:
    3.44 - "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
    3.45 +     "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
    3.46  apply (induct le xs rule: qsort.induct)
    3.47   apply simp
    3.48  apply simp
    3.49 @@ -35,28 +37,23 @@
    3.50  done
    3.51  
    3.52  
    3.53 -(*Version two: type classes*)
    3.54 +subsection{*Version 2:type classes*}
    3.55  
    3.56  consts quickSort :: "('a::linorder) list => 'a list"
    3.57  
    3.58  recdef quickSort "measure size"
    3.59 -"quickSort []   = []"
    3.60 -"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
    3.61 +    "quickSort []   = []"
    3.62 +    "quickSort (x#l) = quickSort [y:l. ~ x\<le>y] @ [x] @ quickSort [y:l. x\<le>y]"
    3.63  (hints recdef_simp: length_filter_le[THEN le_less_trans])
    3.64  
    3.65  lemma quickSort_permutes[simp]:
    3.66   "multiset_of (quickSort xs) = multiset_of xs"
    3.67  by (induct xs rule: quickSort.induct) (auto simp: union_ac)
    3.68  
    3.69 -(*Also provable by induction*)
    3.70  lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
    3.71  by(simp add: set_count_greater_0)
    3.72  
    3.73 -lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
    3.74 -apply (induct xs rule: quickSort.induct)
    3.75 - apply simp
    3.76 -apply simp
    3.77 -apply(blast intro: linorder_linear[THEN disjE] order_trans)
    3.78 -done
    3.79 +theorem sorted_quickSort: "sorted (op \<le>) (quickSort xs)"
    3.80 +by (induct xs rule: quickSort.induct, auto)
    3.81  
    3.82  end
     4.1 --- a/src/HOL/ex/Sorting.thy	Fri Apr 22 15:10:42 2005 +0200
     4.2 +++ b/src/HOL/ex/Sorting.thy	Fri Apr 22 17:32:03 2005 +0200
     4.3 @@ -2,11 +2,13 @@
     4.4      ID:         $Id$
     4.5      Author:     Tobias Nipkow
     4.6      Copyright   1994 TU Muenchen
     4.7 -
     4.8 -Specification of sorting
     4.9  *)
    4.10  
    4.11 -theory Sorting = Main + Multiset:
    4.12 +header{*Sorting: Basic Theory*}
    4.13 +
    4.14 +theory Sorting
    4.15 +imports Main Multiset
    4.16 +begin
    4.17  
    4.18  consts
    4.19    sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    4.20 @@ -19,22 +21,21 @@
    4.21  
    4.22  primrec
    4.23    "sorted le [] = True"
    4.24 -  "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
    4.25 +  "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
    4.26  
    4.27  
    4.28  constdefs
    4.29    total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    4.30 -   "total r == (ALL x y. r x y | r y x)"
    4.31 +   "total r == (\<forall>x y. r x y | r y x)"
    4.32    
    4.33    transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    4.34 -   "transf f == (ALL x y z. f x y & f y z --> f x z)"
    4.35 +   "transf f == (\<forall>x y z. f x y & f y z --> f x z)"
    4.36  
    4.37  
    4.38  
    4.39  (* Equivalence of two definitions of `sorted' *)
    4.40  
    4.41 -lemma sorted1_is_sorted:
    4.42 - "transf(le) ==> sorted1 le xs = sorted le xs";
    4.43 +lemma sorted1_is_sorted: "transf(le) ==> sorted1 le xs = sorted le xs";
    4.44  apply(induct xs)
    4.45   apply simp
    4.46  apply(simp split: list.split)
    4.47 @@ -42,9 +43,9 @@
    4.48  apply(blast)
    4.49  done
    4.50  
    4.51 -lemma sorted_append[simp]:
    4.52 - "sorted le (xs@ys) = (sorted le xs \<and> sorted le ys \<and>
    4.53 -                       (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
    4.54 +lemma sorted_append [simp]:
    4.55 + "sorted le (xs@ys) = 
    4.56 +  (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
    4.57  by (induct xs, auto)
    4.58  
    4.59  end