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