58644
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
58889
|
3 |
section {* Bubblesort *}
|
58644
|
4 |
|
|
5 |
theory Bubblesort
|
|
6 |
imports "~~/src/HOL/Library/Multiset"
|
|
7 |
begin
|
|
8 |
|
|
9 |
text{* This is \emph{a} version of bubblesort. *}
|
|
10 |
|
|
11 |
context linorder
|
|
12 |
begin
|
|
13 |
|
|
14 |
fun bubble_min where
|
|
15 |
"bubble_min [] = []" |
|
|
16 |
"bubble_min [x] = [x]" |
|
|
17 |
"bubble_min (x#xs) =
|
|
18 |
(case bubble_min xs of y#ys \<Rightarrow> if x>y then y#x#ys else x#y#ys)"
|
|
19 |
|
|
20 |
lemma size_bubble_min: "size(bubble_min xs) = size xs"
|
|
21 |
by(induction xs rule: bubble_min.induct) (auto split: list.split)
|
|
22 |
|
|
23 |
lemma bubble_min_eq_Nil_iff[simp]: "bubble_min xs = [] \<longleftrightarrow> xs = []"
|
|
24 |
by (metis length_0_conv size_bubble_min)
|
|
25 |
|
|
26 |
lemma bubble_minD_size: "bubble_min (xs) = ys \<Longrightarrow> size xs = size ys"
|
|
27 |
by(auto simp: size_bubble_min)
|
|
28 |
|
|
29 |
function (sequential) bubblesort where
|
|
30 |
"bubblesort [] = []" |
|
|
31 |
"bubblesort [x] = [x]" |
|
|
32 |
"bubblesort xs = (case bubble_min xs of y#ys \<Rightarrow> y # bubblesort ys)"
|
|
33 |
by pat_completeness auto
|
|
34 |
|
|
35 |
termination
|
|
36 |
proof
|
|
37 |
show "wf(measure size)" by simp
|
|
38 |
next
|
|
39 |
fix x1 x2 y :: 'a fix xs ys :: "'a list"
|
|
40 |
show "bubble_min(x1#x2#xs) = y#ys \<Longrightarrow> (ys, x1#x2#xs) \<in> measure size"
|
|
41 |
by(auto simp: size_bubble_min dest!: bubble_minD_size split: list.splits if_splits)
|
|
42 |
qed
|
|
43 |
|
60515
|
44 |
lemma mset_bubble_min: "mset (bubble_min xs) = mset xs"
|
58644
|
45 |
apply(induction xs rule: bubble_min.induct)
|
|
46 |
apply simp
|
|
47 |
apply simp
|
|
48 |
apply (auto simp: add_eq_conv_ex split: list.split)
|
|
49 |
done
|
|
50 |
|
|
51 |
lemma bubble_minD_mset:
|
60515
|
52 |
"bubble_min (xs) = ys \<Longrightarrow> mset xs = mset ys"
|
58644
|
53 |
by(auto simp: mset_bubble_min)
|
|
54 |
|
|
55 |
lemma mset_bubblesort:
|
60515
|
56 |
"mset (bubblesort xs) = mset xs"
|
58644
|
57 |
apply(induction xs rule: bubblesort.induct)
|
|
58 |
apply simp
|
|
59 |
apply simp
|
|
60 |
by(auto split: list.splits if_splits dest: bubble_minD_mset)
|
60515
|
61 |
(metis add_eq_conv_ex mset_bubble_min mset.simps(2))
|
58644
|
62 |
|
|
63 |
lemma set_bubblesort: "set (bubblesort xs) = set xs"
|
60515
|
64 |
by(rule mset_bubblesort[THEN mset_eq_setD])
|
58644
|
65 |
|
|
66 |
lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z"
|
|
67 |
apply(induction xs arbitrary: y ys z rule: bubble_min.induct)
|
|
68 |
apply simp
|
|
69 |
apply simp
|
|
70 |
apply (fastforce split: list.splits if_splits dest!: sym[of "a#b" for a b])
|
|
71 |
done
|
|
72 |
|
|
73 |
lemma sorted_bubblesort: "sorted(bubblesort xs)"
|
|
74 |
apply(induction xs rule: bubblesort.induct)
|
|
75 |
apply simp
|
|
76 |
apply simp
|
|
77 |
apply (fastforce simp: set_bubblesort split: list.split if_splits
|
|
78 |
intro!: sorted.Cons dest: bubble_min_min)
|
|
79 |
done
|
|
80 |
|
|
81 |
end
|
|
82 |
|
|
83 |
end
|