src/HOL/ex/Quicksort.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 62430 9527ff088c15 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Author:     Tobias Nipkow
```
```     2     Copyright   1994 TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>Quicksort with function package\<close>
```
```     6
```
```     7 theory Quicksort
```
```     8 imports "~~/src/HOL/Library/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. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
```
```    17
```
```    18 lemma [code]:
```
```    19   "quicksort []     = []"
```
```    20   "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
```
```    21   by (simp_all add: not_le)
```
```    22
```
```    23 lemma quicksort_permutes [simp]:
```
```    24   "mset (quicksort xs) = mset xs"
```
```    25   by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
```
```    26
```
```    27 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
```
```    28 proof -
```
```    29   have "set_mset (mset (quicksort xs)) = set_mset (mset xs)"
```
```    30     by simp
```
```    31   then show ?thesis by (simp only: set_mset_mset)
```
```    32 qed
```
```    33
```
```    34 lemma sorted_quicksort: "sorted (quicksort xs)"
```
```    35   by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
```
```    36
```
```    37 theorem sort_quicksort:
```
```    38   "sort = quicksort"
```
```    39   by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
```
```    40
```
```    41 end
```
```    42
```
```    43 end
```