equal
deleted
inserted
replaced
56 "mset (bubblesort xs) = mset xs" |
56 "mset (bubblesort xs) = mset xs" |
57 apply(induction xs rule: bubblesort.induct) |
57 apply(induction xs rule: bubblesort.induct) |
58 apply simp |
58 apply simp |
59 apply simp |
59 apply simp |
60 by(auto split: list.splits if_splits dest: bubble_minD_mset) |
60 by(auto split: list.splits if_splits dest: bubble_minD_mset) |
61 (metis add_eq_conv_ex mset_bubble_min mset.simps(2)) |
|
62 |
61 |
63 lemma set_bubblesort: "set (bubblesort xs) = set xs" |
62 lemma set_bubblesort: "set (bubblesort xs) = set xs" |
64 by(rule mset_bubblesort[THEN mset_eq_setD]) |
63 by(rule mset_bubblesort[THEN mset_eq_setD]) |
65 |
64 |
66 lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z" |
65 lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z" |