src/HOL/Library/Quicksort.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 30738 0842e906300c child 37075 a680ce27aa56 permissions -rw-r--r--
cleaned up some proofs
```     1 (*  Author:     Tobias Nipkow
```
```     2     Copyright   1994 TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header{*Quicksort*}
```
```     6
```
```     7 theory Quicksort
```
```     8 imports Main Multiset
```
```     9 begin
```
```    10
```
```    11 context linorder
```
```    12 begin
```
```    13
```
```    14 fun quicksort :: "'a list \<Rightarrow> 'a list" where
```
```    15 "quicksort []     = []" |
```
```    16 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
```
```    17
```
```    18 lemma quicksort_permutes [simp]:
```
```    19   "multiset_of (quicksort xs) = multiset_of xs"
```
```    20 by (induct xs rule: quicksort.induct) (auto simp: union_ac)
```
```    21
```
```    22 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
```
```    23 by(simp add: set_count_greater_0)
```
```    24
```
```    25 lemma sorted_quicksort: "sorted(quicksort xs)"
```
```    26 apply (induct xs rule: quicksort.induct)
```
```    27  apply simp
```
```    28 apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
```
```    29 apply (metis leD le_cases le_less_trans)
```
```    30 done
```
```    31
```
```    32 end
```
```    33
```
```    34 end
```