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