Isabelle HOL中归并排序时间复杂度证明及简化求助

我在Isabelle/HOL中尝试证明归并排序算法的时间复杂度，代码如下：

theory Merge_Sort_Time
  imports Complex_Main "HOL-ex.BigO"
begin

fun merge :: "'a::linorder list ⇒ 'a list ⇒ 'a list" where
  "merge xs [] = xs"
| "merge [] ys = ys"
| "merge (x#xs) (y#ys) = (if x ≤ y then x # merge xs (y#ys)
                                   else y # merge (x#xs) ys)"

fun msort :: "'a::linorder list ⇒ 'a list" where
  "msort [] = []"
| "msort [x] = [x]"
| "msort xs = (let n = length xs div 2 in
               merge (msort (take n xs)) (msort (drop n xs)))"

fun msort_time :: "nat ⇒ real" where
  "msort_time 0 = 0"
| "msort_time (Suc 0) = 1"
| "msort_time n = msort_time (n div 2) + msort_time (n - n div 2) + n"

lemma msort_time_upper_bound:
  "msort_time ∈ O(λn. n * log 2 n)"
  sorry

end

问题：BigO定义不符合渐进复杂度要求 #

上述引理无法证明，原因是HOL-ex.BigO中的BigO定义是全局约束：

msort_time ∈ {h. ∃c. ∀x. ¦h x¦ ≤ c * ¦x * log 2 x¦}

当n=1时，log 2 1 = 0，但msort_time 1 = 1，显然不满足该约束。而正确的渐进BigO定义应该是仅对足够大的n成立：

msort_time ∈ {h. ∃c n₀. ∀x ≥ n₀. ¦h x¦ ≤ c * ¦x * log 2 x¦}

想询问是否有其他符合渐进复杂度定义的BigO符号库可以使用？

尝试的证明及停滞点 #

我尝试直接证明一个限定n≥2的引理，但卡在最后一步：

lemma sum_log:
  "x > 0 ⟹ y > 0 ⟹
   x * log 2 x + y * log 2 y ≤ (x + y) * log 2 (x + y)"
  by (simp add: add_mono_thms_linordered_semiring(1) distrib_right)

lemma msort_time_upper_bound:
  "∃c. ∀n ≥ 2. msort_time n ≤ c * n * log 2 n"
proof
  let ?c = 3
  show "∀n ≥ 2. msort_time n ≤ ?c * real n * log 2 n"
  proof
    fix n :: nat
    show "n ≥ 2 ⟶ msort_time n ≤ ?c * real n * log 2 n"
    proof
      assume "n ≥ 2"
      then show "msort_time n ≤ ?c * real n * log 2 n"
      proof (induct n rule: less_induct)
        case (less n)
        then show ?case
        proof -
          consider
            (n1) "n < 2" |
            (n2) "n = 2" |
            (n3) "n = 3" |
            (n4) "n ≥ 4"
            by arith
          then show "msort_time n ≤ ?c * real n * log 2 n"
          proof (cases)
            case n1
            then show ?thesis by (simp add: less.prems less_le_not_le)
          next
            case n2
            then show ?thesis by (simp add: numeral_2_eq_2)
          next
            case n3
            then have "msort_time n = 8"
              by (induct rule: msort_time.induct; simp)
            also have "... < ?c * n" by (simp add: n3)
            also have "... < ?c * n * log 2 n" by (simp add: n3)
            finally show ?thesis by linarith
          next
            case n4

            let ?a = "n div 2"
            let ?b = "n - ?a"

            have a: "2 ≤ ?a ∧ ?a < n" using n4 by simp_all
            have b: "2 ≤ ?b ∧ ?b < n" using n4 by simp_all

            have IH_a: "msort_time ?a ≤ ?c * real ?a * log 2 ?a"
              using a less.hyps by blast
            have IH_b: "msort_time ?b ≤ ?c * real ?b * log 2 ?b"
              using b less.hyps by blast

            have "msort_time n = msort_time ?a + msort_time ?b + n"
              by (metis dual_order.strict_iff_not less.prems lessI msort_time.elims not_numeral_le_zero numeral_2_eq_2)

            also have "... ≤ ?c * real ?a * log 2 ?a + ?c * real ?b * log 2 ?b + n"
              using IH_a IH_b by argo

            also have "... ≤ ?c * (real ?a + real ?b) * log 2 (real ?a + real ?b) + n"
              using sum_log[of ?a ?b] b by linarith

            also have "... ≤ ?c * n * log 2 n + n"
              by simp

            also have "... ≤ 2 * ?c * n * log 2 n"
              using n4 mult_ge1_I by simp

            finally show ?thesis
              sorry
          qed
        qed
      qed
    qed
  qed
qed

请求协助 #

1. 完成上述引理的最后一步证明；
2. 提供简化证明结构的建议，减少嵌套证明的层数。

内容的提问来源于stack exchange，提问作者Denis