Theory Efficient_Sort

theory Efficient_Sort
imports Multiset

theory Efficient_Sort
imports
begin

section

text
subsection

context
fixes key ::
begin

text
fun sequences ::
and asc ::
and desc ::
where

|
|
|
|
|
|

fun merge ::
where

|
|

fun merge_pairs ::
where

|

lemma length_merge [simp]:

by (induct xs ys rule: merge.induct) simp_all

lemma length_merge_pairs [simp]:

by (induct xs rule: merge_pairs.induct) simp_all

fun merge_all ::
where

|
|

fun msort_key ::
where

subsection

definition

lemma ascP_Cons [simp]:  by (simp add: ascP_def)

lemma ascP_comp_Cons [simp]:
by (auto simp: ascP_def simp flip: append_Cons)

lemma ascP_comp_append:
by (auto simp: ascP_def)

lemma ascP_f_singleton:
assumes
shows
using assms [unfolded ascP_def, THEN spec, THEN spec, of  ] by simp

lemma ascP_f_Cons:
assumes
shows
using assms [unfolded ascP_def, THEN spec, THEN spec, of  ] by simp

lemma
shows length_sequences:
and length_asc:
and length_desc:
by (induct xs and a f ys and a xs ys rule: sequences_asc_desc.induct) auto

lemma length_concat_merge_pairs [simp]:

by (induct xss rule: merge_pairs.induct) simp_all

subsection

lemma mset_merge [simp]:

by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)

lemma set_merge [simp]:

by (simp flip: set_mset_mset)

lemma mset_concat_merge_pairs [simp]:

by (induct xs rule: merge_pairs.induct) (auto simp: ac_simps)

lemma set_concat_merge_pairs [simp]:

by (simp flip: set_mset_mset)

lemma mset_merge_all [simp]:

by (induct xs rule: merge_all.induct) (simp_all add: ac_simps)

lemma set_merge_all [simp]:

by (simp flip: set_mset_mset)

lemma
shows mset_seqeuences [simp]:
and mset_asc:
and mset_desc:
by (induct xs and x f ys and x xs ys rule: sequences_asc_desc.induct)
(auto simp: ascP_f_singleton)

lemma mset_msort_key:

by (auto)

lemma sorted_merge [simp]:
assumes  and
shows
using assms by (induct xs ys rule: merge.induct) (auto)

lemma sorted_merge_pairs [simp]:
assumes
shows
using assms by (induct xs rule: merge_pairs.induct) simp_all

lemma sorted_merge_all:
assumes
shows
using assms by (induct xs rule: merge_all.induct) simp_all

lemma
shows sorted_sequences:
and sorted_asc:
and sorted_desc:
by (induct xs and a f ys and a xs ys rule: sequences_asc_desc.induct)
(auto simp: ascP_f_singleton sorted_append not_less dest: order_trans, fastforce)

lemma sorted_msort_key:

by (unfold msort_key.simps) (intro sorted_merge_all sorted_sequences)

subsection

lemma
shows filter_by_key_sequences [simp]:
and filter_by_key_asc:
and filter_by_key_desc:
proof (induct xs and a f ys and a xs ys rule: sequences_asc_desc.induct)
case (4 a f b bs)
then show ?case
by (auto simp: o_def ascP_f_Cons [where f = f] ascP_comp_append)
next
case (6 a as b bs)
then show ?case
proof (cases )
case True
with 6 have
by (auto simp: less_le order_trans)
then show ?thesis
using True and 6
by (cases , cases )
(auto simp: Cons_eq_append_conv intro!: filter_False)
qed auto
qed auto

lemma filter_by_key_merge_is_append [simp]:
assumes
shows
using assms
by (induct xs ys rule: merge.induct) (auto simp: Cons_eq_append_conv leD intro!: filter_False)

lemma filter_by_key_merge_pairs [simp]:
assumes
shows
using assms by (induct xss rule: merge_pairs.induct) simp_all

lemma filter_by_key_merge_all [simp]:
assumes
shows
using assms by (induct xss rule: merge_all.induct) simp_all

lemma filter_by_key_merge_all_sequences [simp]:

using sorted_sequences [of xs] by simp

lemma msort_key_stable:

by auto

lemma sort_key_msort_key_conv:

using msort_key_stable [of  for x]
by (intro ext properties_for_sort_key mset_msort_key sorted_msort_key)
(metis (mono_tags, lifting) filter_cong)

end

text
declare sort_key_by_quicksort_code [code del]
declare sort_key_msort_key_conv [code]

end