equal
deleted
inserted
replaced
16 "quicksort [] = []" | |
16 "quicksort [] = []" | |
17 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])" |
17 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])" |
18 by pat_completeness auto |
18 by pat_completeness auto |
19 |
19 |
20 termination by (relation "measure size") |
20 termination by (relation "measure size") |
21 (auto simp: length_filter_le [THEN order_class.le_less_trans]) |
21 (auto simp: length_filter_le [THEN preorder_class.le_less_trans]) |
22 |
22 |
23 lemma quicksort_permutes [simp]: |
23 lemma quicksort_permutes [simp]: |
24 "multiset_of (quicksort xs) = multiset_of xs" |
24 "multiset_of (quicksort xs) = multiset_of xs" |
25 by (induct xs rule: quicksort.induct) (auto simp: union_ac) |
25 by (induct xs rule: quicksort.induct) (auto simp: union_ac) |
26 |
26 |