1.1 --- a/src/HOL/ex/Quicksort.thy	Tue Aug 30 17:51:30 2011 +0200
     1.2 +++ b/src/HOL/ex/Quicksort.thy	Tue Aug 30 17:53:03 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Quicksort with function package *}
     1.5  
     1.6  theory Quicksort
     1.7 -imports Main "~~/src/HOL/Library/Multiset"
     1.8 +imports "~~/src/HOL/Library/Multiset"
     1.9  begin
    1.10  
    1.11  context linorder

     2.1 --- a/src/HOL/ex/Sorting.thy	Tue Aug 30 17:51:30 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,51 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Sorting.thy
     2.5 -    Author:     Tobias Nipkow
     2.6 -    Copyright   1994 TU Muenchen
     2.7 -*)
     2.8 -
     2.9 -header{*Sorting: Basic Theory*}
    2.10 -
    2.11 -theory Sorting
    2.12 -imports Main "~~/src/HOL/Library/Multiset"
    2.13 -begin
    2.14 -
    2.15 -consts
    2.16 -  sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    2.17 -  sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    2.18 -
    2.19 -primrec
    2.20 -  "sorted1 le [] = True"
    2.21 -  "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
    2.22 -                        sorted1 le xs)"
    2.23 -
    2.24 -primrec
    2.25 -  "sorted le [] = True"
    2.26 -  "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
    2.27 -
    2.28 -
    2.29 -definition
    2.30 -  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
    2.31 -   "total r = (\<forall>x y. r x y | r y x)"
    2.32 -  
    2.33 -definition
    2.34 -  transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
    2.35 -   "transf f = (\<forall>x y z. f x y & f y z --> f x z)"
    2.36 -
    2.37 -
    2.38 -
    2.39 -(* Equivalence of two definitions of `sorted' *)
    2.40 -
    2.41 -lemma sorted1_is_sorted: "transf(le) ==> sorted1 le xs = sorted le xs";
    2.42 -apply(induct xs)
    2.43 - apply simp
    2.44 -apply(simp split: list.split)
    2.45 -apply(unfold transf_def);
    2.46 -apply(blast)
    2.47 -done
    2.48 -
    2.49 -lemma sorted_append [simp]:
    2.50 -  "sorted le (xs@ys) = 
    2.51 -    (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
    2.52 -  by (induct xs) auto
    2.53 -
    2.54 -end