src/HOL/ex/Bubblesort.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58644 8171ef293634
child 60515 484559628038
permissions -rw-r--r--
modernized header uniformly as section;
     1 (* Author: Tobias Nipkow *)
     2 
     3 section {* Bubblesort *}
     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 
    44 lemma mset_bubble_min: "multiset_of (bubble_min xs) = multiset_of xs"
    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:
    52   "bubble_min (xs) = ys \<Longrightarrow> multiset_of xs = multiset_of ys"
    53 by(auto simp: mset_bubble_min)
    54 
    55 lemma mset_bubblesort:
    56   "multiset_of (bubblesort xs) = multiset_of xs"
    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   (metis add_eq_conv_ex mset_bubble_min multiset_of.simps(2))
    62 
    63 lemma set_bubblesort: "set (bubblesort xs) = set xs"
    64 by(rule mset_bubblesort[THEN multiset_of_eq_setD])
    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