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