equal
deleted
inserted
replaced
13 |
13 |
14 recdef qsort "measure (size o snd)" |
14 recdef qsort "measure (size o snd)" |
15 "qsort(le, []) = []" |
15 "qsort(le, []) = []" |
16 "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @ |
16 "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @ |
17 qsort(le, [y:xs . le x y])" |
17 qsort(le, [y:xs . le x y])" |
18 (hints recdef_simp: length_filter[THEN le_less_trans]) |
18 (hints recdef_simp: length_filter_le[THEN le_less_trans]) |
19 |
19 |
20 lemma qsort_permutes[simp]: |
20 lemma qsort_permutes[simp]: |
21 "multiset (qsort(le,xs)) x = multiset xs x" |
21 "multiset (qsort(le,xs)) x = multiset xs x" |
22 by (induct le xs rule: qsort.induct, auto) |
22 by (induct le xs rule: qsort.induct, auto) |
23 |
23 |
41 consts quickSort :: "('a::linorder) list => 'a list" |
41 consts quickSort :: "('a::linorder) list => 'a list" |
42 |
42 |
43 recdef quickSort "measure size" |
43 recdef quickSort "measure size" |
44 "quickSort [] = []" |
44 "quickSort [] = []" |
45 "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]" |
45 "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]" |
46 (hints recdef_simp: length_filter[THEN le_less_trans]) |
46 (hints recdef_simp: length_filter_le[THEN le_less_trans]) |
47 |
47 |
48 lemma quickSort_permutes[simp]: |
48 lemma quickSort_permutes[simp]: |
49 "multiset (quickSort xs) z = multiset xs z" |
49 "multiset (quickSort xs) z = multiset xs z" |
50 by (induct xs rule: quickSort.induct) auto |
50 by (induct xs rule: quickSort.induct) auto |
51 |
51 |