tuned import;
discontinued obsolete Sorting.thy (cf. 4d57f872dc2c);
--- a/src/HOL/ex/Quicksort.thy Tue Aug 30 17:51:30 2011 +0200
+++ b/src/HOL/ex/Quicksort.thy Tue Aug 30 17:53:03 2011 +0200
@@ -5,7 +5,7 @@
header {* Quicksort with function package *}
theory Quicksort
-imports Main "~~/src/HOL/Library/Multiset"
+imports "~~/src/HOL/Library/Multiset"
begin
context linorder
--- a/src/HOL/ex/Sorting.thy Tue Aug 30 17:51:30 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(* Title: HOL/ex/Sorting.thy
- Author: Tobias Nipkow
- Copyright 1994 TU Muenchen
-*)
-
-header{*Sorting: Basic Theory*}
-
-theory Sorting
-imports Main "~~/src/HOL/Library/Multiset"
-begin
-
-consts
- sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
- sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-
-primrec
- "sorted1 le [] = True"
- "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
- sorted1 le xs)"
-
-primrec
- "sorted le [] = True"
- "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
-
-
-definition
- total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
- "total r = (\<forall>x y. r x y | r y x)"
-
-definition
- transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
- "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";
-apply(induct xs)
- apply simp
-apply(simp split: list.split)
-apply(unfold transf_def);
-apply(blast)
-done
-
-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