author | haftmann |
Fri, 14 Jun 2019 08:34:28 +0000 | |
changeset 70347 | e5cd5471c18a |
parent 68109 | cebf36c14226 |
permissions | -rw-r--r-- |
58644 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
61343 | 3 |
section \<open>Bubblesort\<close> |
58644 | 4 |
|
5 |
theory Bubblesort |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66110
diff
changeset
|
6 |
imports "HOL-Library.Multiset" |
58644 | 7 |
begin |
8 |
||
61343 | 9 |
text\<open>This is \emph{a} version of bubblesort.\<close> |
58644 | 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 |
|
66110 | 48 |
apply (auto split: list.split) |
58644 | 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) |
|
61 |
||
62 |
lemma set_bubblesort: "set (bubblesort xs) = set xs" |
|
60515 | 63 |
by(rule mset_bubblesort[THEN mset_eq_setD]) |
58644 | 64 |
|
65 |
lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z" |
|
66 |
apply(induction xs arbitrary: y ys z rule: bubble_min.induct) |
|
67 |
apply simp |
|
68 |
apply simp |
|
69 |
apply (fastforce split: list.splits if_splits dest!: sym[of "a#b" for a b]) |
|
70 |
done |
|
71 |
||
72 |
lemma sorted_bubblesort: "sorted(bubblesort xs)" |
|
73 |
apply(induction xs rule: bubblesort.induct) |
|
74 |
apply simp |
|
75 |
apply simp |
|
68109 | 76 |
apply (fastforce simp: set_bubblesort split: list.split if_splits dest: bubble_min_min) |
58644 | 77 |
done |
78 |
||
79 |
end |
|
80 |
||
81 |
end |