src/HOL/Library/Quicksort.thy
 author chaieb Mon Feb 09 17:21:46 2009 +0000 (2009-02-09) changeset 29847 af32126ee729 parent 28041 f496e9f343b7 child 30738 0842e906300c permissions -rw-r--r--
added Determinants to Library
```     1 (*  ID:         \$Id\$
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   1994 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header{*Quicksort*}
```
```     7
```
```     8 theory Quicksort
```
```     9 imports Plain Multiset
```
```    10 begin
```
```    11
```
```    12 context linorder
```
```    13 begin
```
```    14
```
```    15 fun quicksort :: "'a list \<Rightarrow> 'a list" where
```
```    16 "quicksort []     = []" |
```
```    17 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
```
```    18
```
```    19 lemma quicksort_permutes [simp]:
```
```    20   "multiset_of (quicksort xs) = multiset_of xs"
```
```    21 by (induct xs rule: quicksort.induct) (auto simp: union_ac)
```
```    22
```
```    23 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
```
```    24 by(simp add: set_count_greater_0)
```
```    25
```
```    26 lemma sorted_quicksort: "sorted(quicksort xs)"
```
```    27 apply (induct xs rule: quicksort.induct)
```
```    28  apply simp
```
```    29 apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
```
```    30 apply (metis leD le_cases le_less_trans)
```
```    31 done
```
```    32
```
```    33 end
```
```    34
```
```    35 end
```