Theory Challenge1B

section ‹Challenge 1.B›
theory Challenge1B
  imports Challenge1A "HOL-Library.Multiset"
begin

(* TODO: Move *)
lemma mset_concat:
  "mset (concat xs) = fold (+) (map mset xs) {#}"
proof -
  have "mset (concat xs) + a = fold (+) (map mset xs) a" for a
  proof (induction xs arbitrary: a)
    case Nil
    then show ?case
      by auto
  next
    case (Cons x xs)
    show ?case
      using Cons.IH[of "mset x + a", symmetric] by simp
  qed
  from this[of "{#}"] show ?thesis
    by auto
qed

subsection ‹Merging Two Segments›

fun merge :: "'a::{linorder} list ⇒ 'a list ⇒ 'a list" where
   "merge [] l2 = l2"
 | "merge l1 [] = l1"
 | "merge (x1 # l1) (x2 # l2) =
    (if (x1 < x2) then x1 # (merge l1 (x2 # l2)) else x2 # (merge (x1 # l1) l2))"

lemma merge_correct:
  assumes "sorted l1"
  assumes "sorted l2"
  shows "
    sorted (merge l1 l2)
  ∧ mset (merge l1 l2) = mset l1 + mset l2
  ∧ set (merge l1 l2) = set l1 ∪ set l2"
  using assms
proof (induction l1 arbitrary: l2)
  case Nil thus ?case
    by simp
next
  case (Cons x1 l1 l2)
  note IH = Cons.IH

  show ?case
    using Cons.prems
  proof (induction l2)
    case Nil then show ?case
      by simp
  next
    case (Cons x2 l2)
    then show ?case
      using IH by (force split: if_split_asm)
  qed
qed

subsection ‹Merging a List of Segments›

function merge_list :: "'a::{linorder} list list ⇒ 'a list list ⇒ 'a list" where
   "merge_list [] [] = []"
 | "merge_list [] [l] = l"
 | "merge_list (la # acc2) [] = merge_list [] (la # acc2)"
 | "merge_list (la # acc2) [l] = merge_list [] (l # la # acc2)"
 | "merge_list acc2 (l1 # l2 # ls) =
    merge_list ((merge l1 l2) # acc2) ls"
by pat_completeness simp_all
termination by (relation "measure (λ(acc, ls). 3 * length acc + 2 * length ls)"; simp)

lemma merge_list_correct:
assumes "⋀l. l ∈ set ls ⟹ sorted l"
assumes "⋀l. l ∈ set as ⟹ sorted l"
shows "
  sorted (merge_list as ls)
∧ mset (merge_list as ls) = mset (concat (as @ ls))
∧ set (merge_list as ls) = set (concat (as @ ls))"
using assms
proof (induction as ls rule: merge_list.induct)
next
  case (4 la acc2 l)
  then show ?case
    by (auto simp: algebra_simps)
next
  case (5 acc2 l1 l2 ls)
  have "sorted (merge_list (merge l1 l2 # acc2) ls)
    ∧ mset (merge_list (merge l1 l2 # acc2) ls) = mset (concat ((merge l1 l2 # acc2) @ ls))
    ∧ set (merge_list (merge l1 l2 # acc2) ls) = set (concat ((merge l1 l2 # acc2) @ ls))"
    using 5(2-) merge_correct[of l1 l2] by (intro 5(1)) auto
  then show ?case
    using merge_correct[of l1 l2] 5(2-) by auto
qed simp+

subsection ‹GHC-Sort›

definition
  "ghc_sort xs = merge_list [] (map (λys. if decr ys then rev ys else ys) (cuts xs))"

lemma decr_sorted:
  assumes "decr xs"
  shows "sorted (rev xs)"
  using assms by (induction xs rule: decr.induct) (auto simp: sorted_append)

lemma incr_sorted:
  assumes "incr xs"
  shows "sorted xs"
  using assms by (induction xs rule: incr.induct) auto

lemma reverse_phase_sorted:
  "∀ys ∈ set (map (λys. if decr ys then rev ys else ys) (cuts xs)). sorted ys"
  using cuts_incr_decr by (auto intro: decr_sorted incr_sorted)

lemma reverse_phase_elements:
  "set (concat (map (λys. if decr ys then rev ys else ys) (cuts xs))) = set xs"
proof -
  have "set (concat (map (λys. if decr ys then rev ys else ys) (cuts xs)))
    = set (concat (cuts xs))"
    by auto
  also have "… = set xs"
    by (simp add: concat_cuts)
  finally show ?thesis .
qed

lemma reverse_phase_permutation:
  "mset (concat (map (λys. if decr ys then rev ys else ys) (cuts xs))) = mset xs"
proof -
  have "mset (concat (map (λys. if decr ys then rev ys else ys) (cuts xs)))
    = mset (concat (cuts xs))"
    unfolding mset_concat by (auto simp: comp_def intro!: arg_cong2[where f = "fold (+)"])
  also have "… = mset xs"
    by (simp add: concat_cuts)
  finally show ?thesis .
qed

subsection ‹Correctness Lemmas›
text ‹The result is sorted and a permutation of the original elements.›

theorem sorted_ghc_sort:
  "sorted (ghc_sort xs)"
  unfolding ghc_sort_def using reverse_phase_sorted
  by (intro merge_list_correct[THEN conjunct1]) auto

theorem permutation_ghc_sort:
  "mset (ghc_sort xs) = mset xs"
  unfolding ghc_sort_def
  apply (subst merge_list_correct[THEN conjunct2])
  subgoal
    using reverse_phase_sorted by auto
  subgoal
    using reverse_phase_sorted by auto
  apply (subst (2) reverse_phase_permutation[symmetric])
  apply simp
  done

corollary elements_ghc_sort: "set (ghc_sort xs) = set xs"
  using permutation_ghc_sort by (metis set_mset_mset)

subsection ‹Executable Code›  
export_code ghc_sort checking SML Scala OCaml? Haskell?

value [code] "ghc_sort [1,2,7,3,5,6,9,8,4]"

end