Theory Karatsuba.Karatsuba

section "Karatsuba Multiplication"

theory Karatsuba
imports "../Binary_Representations/Nat_LSBF" "../Binary_Representations/Int_LSBF" "../Estimation_Method"
begin

text "This theory contains an implementation of the Karatsuba Multiplication on type @{type nat_lsbf}."

definition abs_diff :: "nat_lsbf  nat_lsbf  nat_lsbf" where
"abs_diff x y = (x -n y) +n (y -n x)"

lemma abs_diff_correct: "int (to_nat (abs_diff x y)) = abs (int (to_nat x) - int (to_nat y))"
  unfolding abs_diff_def by (simp add: add_nat_correct subtract_nat_correct)

lemma abs_diff_length: "length (abs_diff xs ys)  max (length xs) (length ys)"
proof (cases "compare_nat xs ys")
  case True
  then have "xs -n ys = []" by (simp add: subtract_nat_def)
  then have "abs_diff xs ys = ys -n xs" by (simp add: abs_diff_def add_nat_def)
  then show ?thesis using length_subtract_nat_le[of ys xs] by simp
next
  case False
  then have "ys n xs" by (simp only: compare_nat_correct)
  then have "ys -n xs = []" by (simp add: subtract_nat_def)
  then have "abs_diff xs ys = xs -n ys" by (simp add: abs_diff_def add_nat_com add_nat_def)
  then show ?thesis using length_subtract_nat_le[of xs ys] by simp
qed

text "For small inputs, implementations of Karatsuba Multiplication usually switch to grid
multiplication. The threshold does not matter for the asymptotic running time, hence we will just
arbitrarily choose @{term 42::nat}."

definition karatsuba_lower_bound :: nat where
"karatsuba_lower_bound  42"

lemma karatsuba_lower_bound_requirement:
  "karatsuba_lower_bound  1"
  unfolding karatsuba_lower_bound_def by simp

text "A first version of the algorithm assumes the input numbers have a length which is a power of 2.
The function @{term karatsuba_on_power_of_2_length} takes the specified length as additional first
argument."

fun karatsuba_on_power_of_2_length :: "nat  nat_lsbf  nat_lsbf  nat_lsbf" where
"karatsuba_on_power_of_2_length k x y =
(if k  karatsuba_lower_bound
then x *n y
else let
    (x0, x1) = split x;
    (y0, y1) = split y;
    k_div_2 = (k div 2);
    prod0 = karatsuba_on_power_of_2_length k_div_2 x0 y0;
    prod1 = karatsuba_on_power_of_2_length k_div_2 x1 y1;
    prod2 = karatsuba_on_power_of_2_length k_div_2
      (fill k_div_2 (abs_diff x0 x1))
      (fill k_div_2 (abs_diff y0 y1));
    add01 = prod0 +n prod1;
    r = (if (x1 n x0) = (y1 n y0)
        then add01 -n prod2
        else add01 +n prod2)
  in prod0 +n (r >>n k_div_2) +n (prod1 >>n k))"

declare karatsuba_on_power_of_2_length.simps[simp del]

locale karatsuba_context =
  fixes k l :: nat
  fixes x y :: nat_lsbf
  assumes k_power_of_2: "k = 2 ^ l"
  assumes length_x: "length x = k"
  assumes length_y: "length y = k"
  assumes recursion_condition: "¬ k  karatsuba_lower_bound"
begin

definition x0 where "x0 = fst (split x)"
definition x1 where "x1 = snd (split x)"
definition y0 where "y0 = fst (split y)"
definition y1 where "y1 = snd (split y)"
definition k_div_2 where "k_div_2 = k div 2"
definition prod0 where "prod0 = karatsuba_on_power_of_2_length k_div_2 x0 y0"
definition prod1 where "prod1 = karatsuba_on_power_of_2_length k_div_2 x1 y1"
definition prod2 where "prod2 = karatsuba_on_power_of_2_length k_div_2
      (fill k_div_2 (abs_diff x0 x1))
      (fill k_div_2 (abs_diff y0 y1))"
definition add01 where "add01 = prod0 +n prod1"
definition r where "r = (if (x1 n x0) = (y1 n y0)
        then add01 -n prod2
        else add01 +n prod2)"

lemma split_x: "split x = (x0, x1)" using x0_def x1_def by simp
lemma split_y: "split y = (y0, y1)" using y0_def y1_def by simp

lemmas defs1 = split_x split_y
lemmas defs2 = prod0_def prod1_def prod2_def k_div_2_def add01_def r_def

lemma recursive: "karatsuba_on_power_of_2_length k x y =
  prod0 +n (r >>n k_div_2) +n (prod1 >>n k)"
  unfolding karatsuba_on_power_of_2_length.simps[of k x y]
  using defs1 defs2 recursion_condition
  by (simp only: if_False Let_def case_prod_conv)

lemma l_ge_1: "l  1"
  using karatsuba_lower_bound_requirement recursion_condition k_power_of_2
  by (cases l; simp)

lemma k_even: "k mod 2 = 0"
  using k_power_of_2 l_ge_1 by simp

lemma k_div_2: "k_div_2 = 2 ^ (l - 1)"
  unfolding k_div_2_def using k_power_of_2 l_ge_1 by (simp add: power_diff)

lemma k_div_2_less_k: "k_div_2 < k"
  unfolding k_div_2_def using k_power_of_2 by simp

lemma length_x_split: "length x0 = k_div_2" "length x1 = k_div_2"
  unfolding k_div_2_def using k_even length_split[OF _ split_x] length_x by argo+

lemma length_y_split: "length y0 = k_div_2" "length y1 = k_div_2"
  unfolding k_div_2_def using k_even length_split[OF _ split_y] length_y by argo+

lemma length_abs_diff_x0_x1: "length (abs_diff x0 x1)  k_div_2"
  using abs_diff_length[of x0 x1] length_x_split by simp
lemma length_fill_abs_diff_x0_x1: "length (fill k_div_2 (abs_diff x0 x1)) = k_div_2"
  by (intro length_fill length_abs_diff_x0_x1)

lemma length_abs_diff_y0_y1: "length (abs_diff y0 y1)  k_div_2"
  using abs_diff_length[of y0 y1] length_y_split by simp
lemma length_fill_abs_diff_y0_y1: "length (fill k_div_2 (abs_diff y0 y1)) = k_div_2"
  by (intro length_fill length_abs_diff_y0_y1)

lemmas IH_prems1 = recursion_condition split_x[symmetric] refl split_y[symmetric] refl k_div_2_def
    k_div_2 length_x_split(1) length_y_split(1)

lemmas IH_prems2 = recursion_condition split_x[symmetric] refl split_y[symmetric] refl k_div_2_def
    prod0_def k_div_2 length_x_split(2) length_y_split(2)

lemmas IH_prems3 = recursion_condition split_x[symmetric] refl split_y[symmetric] refl k_div_2_def
    prod0_def prod1_def k_div_2 length_fill_abs_diff_x0_x1 length_fill_abs_diff_y0_y1

end

lemma karatsuba_on_power_of_2_length_correct:
  assumes "k = 2 ^ l"
  assumes "length x = k" "length y = k"
  shows "to_nat (karatsuba_on_power_of_2_length k x y) = to_nat x * to_nat y"
using assms proof (induction k x y arbitrary: l rule: karatsuba_on_power_of_2_length.induct)
  case (1 k x y l)
  show ?case
  proof (cases "k  karatsuba_lower_bound")
    case True
    then show ?thesis
      unfolding karatsuba_on_power_of_2_length.simps[of k x y]
      by (simp add: grid_mul_nat_correct)
  next
    case False
    then interpret r: karatsuba_context k l x y using "1.prems"
      by (unfold_locales; simp)
    from r.l_ge_1 obtain l' where "l = Suc l'"
      by (metis less_eqE plus_1_eq_Suc)
    then have "k div 2 = 2 ^ l'" using k = 2 ^ l by simp

    have to_nat_x: "to_nat x = to_nat r.x0 + 2 ^ (k div 2) * to_nat r.x1"
      unfolding r.k_div_2_def[symmetric]
      using app_split[OF r.split_x] to_nat_app[of r.x0 r.x1] r.length_x_split by algebra

    have to_nat_y: "to_nat y = to_nat r.y0 + 2 ^ (k div 2) * to_nat r.y1"
      unfolding r.k_div_2_def[symmetric]
      using app_split[OF r.split_y] to_nat_app[of r.y0 r.y1] r.length_y_split by algebra

    have 4: "to_nat r.prod0 = to_nat r.x0 * to_nat r.y0"
      unfolding r.prod0_def
      by (intro 1(1)[OF r.IH_prems1])
    have 5: "to_nat r.prod1 = to_nat r.x1 * to_nat r.y1"
      unfolding r.prod1_def
      by (intro 1(2)[OF r.IH_prems2])
    have "to_nat r.prod2 = to_nat (fill r.k_div_2 (abs_diff r.x0 r.x1)) * to_nat (fill r.k_div_2 (abs_diff r.y0 r.y1))"
      unfolding r.prod2_def
      by (intro 1(3)[OF r.IH_prems3])
    hence "int (to_nat r.prod2) = abs (int (to_nat r.x0) - int (to_nat r.x1)) * abs (int (to_nat r.y0) - int (to_nat r.y1))"
      using abs_diff_correct by simp
    then have "int (to_nat r.prod2) = abs ((int (to_nat r.x0) - int (to_nat r.x1)) * (int (to_nat r.y0) - int (to_nat r.y1)))"
      by (subst abs_mult, assumption)
    then have 6: "(if (compare_nat r.x1 r.x0) = (compare_nat r.y1 r.y0) then int (to_nat r.prod2) else - int (to_nat r.prod2)) = (int (to_nat r.x0) - int (to_nat r.x1)) * (int (to_nat r.y0) - int (to_nat r.y1))"
      apply (cases "to_nat r.x0  to_nat r.x1"; cases "to_nat r.y0  to_nat r.y1")
      by (simp_all add: compare_nat_correct mult_nonneg_nonpos mult_nonneg_nonpos2 mult_nonpos_nonpos)

    have 7: "int (to_nat r.r) = int (to_nat r.x0) * int (to_nat r.y1) + int (to_nat r.x1) * int (to_nat r.y0)"
    proof (cases "(r.x1 n r.x0) = (r.y1 n r.y0)")
      case True
      then have int_p: "int (to_nat r.r) = int (to_nat r.prod0 + to_nat r.prod1 - to_nat r.prod2)"
        unfolding r.r_def r.add01_def
        by (simp add: subtract_nat_correct add_nat_correct)
      have int_prod2: "int (to_nat r.prod2) = (int (to_nat r.x0) - int (to_nat r.x1)) * (int (to_nat r.y0) - int (to_nat r.y1))"
        using 6 True by simp
      have "- (int (to_nat r.x0) * int (to_nat r.y1))  int (to_nat r.x1) * int (to_nat r.y0)"
        apply (intro order.trans[of "- (int (to_nat r.x0) * int (to_nat r.y1))" 0 "int (to_nat r.x1) * int (to_nat r.y0)"])
        by simp_all
      then have "to_nat r.prod0 + to_nat r.prod1  to_nat r.prod2"
        apply (intro iffD1[OF zle_int])
        by (simp add: 4 5 int_prod2 left_diff_distrib right_diff_distrib)
      then have "int (to_nat r.r) = int (to_nat r.prod0) + int (to_nat r.prod1) - int (to_nat r.prod2)"
        using int_p by simp
      then show ?thesis using int_prod2 by (simp add: left_diff_distrib right_diff_distrib 4 5)
    next
      case False
      then have "int (to_nat r.r) = int (to_nat r.prod0) + int (to_nat r.prod1) + int (to_nat r.prod2)"
        unfolding r.r_def
        by (simp add: add_nat_correct r.add01_def)
      moreover from False 6 have "- int (to_nat r.prod2) = (int (to_nat r.x0) - int (to_nat r.x1)) * (int (to_nat r.y0) - int (to_nat r.y1))"
        by simp
      then have "int (to_nat r.prod2) = - (int (to_nat r.x0) - int (to_nat r.x1)) * (int (to_nat r.y0) - int (to_nat r.y1))"
        by linarith
      ultimately show ?thesis by (simp add: 4 5 left_diff_distrib right_diff_distrib)
    qed

    (* the main proof *)
    from r.recursive have "int (to_nat (karatsuba_on_power_of_2_length k x y)) =
      int (to_nat (r.prod0 +n (r.r >>n r.k_div_2) +n (r.prod1 >>n k)))" by simp
    also have "... = int (to_nat r.prod0) + int (to_nat (shift_right r.k_div_2 r.r)) + int (to_nat (shift_right k r.prod1))"
      by (simp add: add_nat_correct)
    also have "... = int (to_nat r.prod0) + int (2 ^ (k div 2) * to_nat r.r) + int (2 ^ k * to_nat r.prod1)"
      by (simp only: to_nat_shift_right r.k_div_2_def)
    also have "... = int (to_nat r.prod0) + 2 ^ (k div 2) * int (to_nat r.r) + 2 ^ k * int (to_nat r.prod1)"
      by simp
    also have "... = int (to_nat r.x0) * int (to_nat r.y0) + 2 ^ (k div 2) * (int (to_nat r.x0) * int (to_nat r.y1) + int (to_nat r.x1) * int (to_nat r.y0)) + 2 ^ k * int (to_nat r.x1) * int (to_nat r.y1)"
      using 7 4 5
      by simp
    also have "... = (int (to_nat r.x0) + 2 ^ (k div 2) * (int (to_nat r.x1)))
      * (int (to_nat r.y0) + 2 ^ (k div 2) * (int (to_nat r.y1)))"
    proof -
      have "2 * (k div 2) = k"
        using r.k_even by force
      have "(int (to_nat r.x0) + 2 ^ (k div 2) * (int (to_nat r.x1)))
          * (int (to_nat r.y0) + 2 ^ (k div 2) * (int (to_nat r.y1)))
        = int (to_nat r.x0) * int (to_nat r.y0)
          + (2::int) ^ (k div 2) * (int (to_nat r.x1)) * (int (to_nat r.y0))
          + (int (to_nat r.x0)) * 2 ^ (k div 2) * (int (to_nat r.y1))
          + (2::int) ^ (k div 2) * (int (to_nat r.x1)) * 2 ^ (k div 2) * (int (to_nat r.y1))"
        using distrib_left[of "(int (to_nat r.x0) + 2 ^ (k div 2) * (int (to_nat r.x1)))" "int (to_nat r.y0)" "2 ^ (k div 2) * (int (to_nat r.y1))"]
        by (simp add: ring_class.ring_distribs(2))
      also have "... = int (to_nat r.x0) * int (to_nat r.y0)
          + (2::int) ^ (k div 2) * (int (to_nat r.x1)) * (int (to_nat r.y0))
          + (int (to_nat r.x0)) * 2 ^ (k div 2) * (int (to_nat r.y1))
          + ((2::int) ^ (k div 2) * 2 ^ (k div 2)) * (int (to_nat r.x1)) * (int (to_nat r.y1))"
        by simp
      also have "(2::int) ^ (k div 2) * 2 ^ (k div 2) = 2 ^ k"
        using power_add[of "2::int" "k div 2" "k div 2", symmetric]
        using 2 * (k div 2) = k
        by simp
      finally have "(int (to_nat r.x0) + 2 ^ (k div 2) * (int (to_nat r.x1)))
          * (int (to_nat r.y0) + 2 ^ (k div 2) * (int (to_nat r.y1)))
        = int (to_nat r.x0) * int (to_nat r.y0)
          + 2 ^ (k div 2) * (int (to_nat r.x1)) * (int (to_nat r.y0))
          + (int (to_nat r.x0)) * 2 ^ (k div 2) * (int (to_nat r.y1))
          + (2::int) ^ k * (int (to_nat r.x1)) * (int (to_nat r.y1))" by simp
      also have "... = int (to_nat r.x0) * int (to_nat r.y0)
          + ((2::int) ^ (k div 2) * (int (to_nat r.x1)) * (int (to_nat r.y0))
          + (2::int) ^ (k div 2) * (int (to_nat r.x0)) * (int (to_nat r.y1)))
          + (2::int) ^ k * (int (to_nat r.x1)) * (int (to_nat r.y1))"
        by simp
      also have "... = int (to_nat r.x0) * int (to_nat r.y0)
          + (2::int) ^ (k div 2) * (int (to_nat r.x1) * int (to_nat r.y0) + int (to_nat r.x0) * int (to_nat r.y1))
          + (2::int) ^ k * (int (to_nat r.x1)) * (int (to_nat r.y1))"
        using distrib_left[of "(2::int) ^ (k div 2)"] by simp
      finally show ?thesis by simp
    qed
    also have "... = int (to_nat x) * int (to_nat y)"
      by (simp add: to_nat_x to_nat_y)
    finally have "int (to_nat (karatsuba_on_power_of_2_length k x y)) = int (to_nat x * to_nat y)"
      by simp
    thus ?thesis by presburger
  qed
qed

function len_kar_bound where
"len_kar_bound l = (if 2 ^ l  karatsuba_lower_bound then 2 * karatsuba_lower_bound else 2 ^ l + len_kar_bound (l - 1) + 4)"
  by pat_completeness auto
termination
  apply (relation "Wellfounded.measure (λl. l)")
  subgoal by simp
  subgoal for l
    using karatsuba_lower_bound_requirement by (cases l; simp)
  done

declare len_kar_bound.simps[simp del]

lemma length_karatsuba_on_power_of_2_aux:
  assumes "k = 2 ^ l"
  assumes "length x = k" "length y = k"
  shows "length (karatsuba_on_power_of_2_length k x y)  len_kar_bound l"
  using assms proof (induction k x y arbitrary: l rule: karatsuba_on_power_of_2_length.induct)
  case (1 k x y)
  then show ?case
  proof (cases "k  karatsuba_lower_bound")
    case True
    then have "karatsuba_on_power_of_2_length k x y = grid_mul_nat x y"
      unfolding karatsuba_on_power_of_2_length.simps[of k x y] by argo
    also have "length ...  length x + length y"
      by (rule length_grid_mul_nat)
    also have "... = 2 * k" using 1 by linarith
    also have "...  len_kar_bound l"
      unfolding len_kar_bound.simps[of l] using "1.prems" True by simp
    finally show ?thesis .
  next
    case False
    then interpret r: karatsuba_context k l x y using "1.prems" by unfold_locales simp_all
    from r.recursive have "length (karatsuba_on_power_of_2_length k x y) =
      length (r.prod0 +n (r.r >>n r.k_div_2) +n
      (r.prod1 >>n k))"
      by argo
    also have "...  max (max (length r.prod0)
            (2 ^ (l - 1) +
             max (max (length r.prod0) (length r.prod1) + 1) (length r.prod2) + 1) + 1)
       (k + length r.prod1) + 1"
      unfolding r.r_def r.add01_def
      apply (estimation estimate: length_add_nat_upper)
      apply (estimation estimate: length_add_nat_upper)
      unfolding length_shift_right r.k_div_2 if_distrib[of length]
      apply (estimation estimate: if_le_max)
      apply (estimation estimate: length_add_nat_upper)
      apply (estimation estimate: length_subtract_nat_le)
      apply (estimation estimate: length_add_nat_upper)
      by simp
    also have "...  max (max (len_kar_bound (l - 1))
          (2 ^ (l - 1) +
           max (max (len_kar_bound (l - 1)) (len_kar_bound (l - 1)) + 1)
            (len_kar_bound (l - 1)) + 1) + 1)
     (k + len_kar_bound (l - 1)) + 1"
      unfolding r.prod0_def r.prod1_def r.prod2_def
      apply (estimation estimate: "1.IH"(1)[OF r.IH_prems1])
      apply (estimation estimate: "1.IH"(2)[OF r.IH_prems2])
      apply (estimation estimate: "1.IH"(3)[OF r.IH_prems3])
      by (rule order.refl)
    also have "... = max (2 ^ (l - 1) + len_kar_bound (l - 1) + 3)
     (2 ^ l + len_kar_bound (l - 1)) + 1"
      unfolding max.idem r.k_power_of_2 by (simp del: One_nat_def)
    also have "...  (2 ^ l + len_kar_bound (l - 1) + 3) + 1"
      apply (intro add_mono order.refl)
      apply (intro max.boundedI)
      subgoal
        apply (intro add_mono order.refl) by simp
      subgoal by simp
      done
    also have "... = len_kar_bound l"
      unfolding len_kar_bound.simps[of l] using False r.k_power_of_2 by simp
    finally show ?thesis .
  qed
qed

lemma len_kar_bound_le: "len_kar_bound l  6 * 2 ^ l + 2 * karatsuba_lower_bound"
proof (induction l rule: less_induct)
  case (less l)
  then show ?case
  proof (cases "2 ^ l  karatsuba_lower_bound")
    case True
    then show ?thesis
      unfolding len_kar_bound.simps[of l] by simp
  next
    case False
    then have "l - 1 < l" using karatsuba_lower_bound_requirement by (cases l; simp)
    then have "l > 0" by simp
    from False have "len_kar_bound l = 2 ^ l + len_kar_bound (l - 1) + 4"
      unfolding len_kar_bound.simps[of l] by argo
    also have "...  2 ^ l + (6 * 2 ^ (l - 1) + 2 * karatsuba_lower_bound) + 4"
      using less[OF l - 1 < l] by simp
    also have "... = 2 * (2 ^ (l - 1)) + (6 * 2 ^ (l - 1) + 2 * karatsuba_lower_bound) + 4"
      unfolding power_Suc[symmetric] Suc_diff_1[OF l > 0] by (rule refl)
    also have "... = 8 * 2 ^ (l - 1) + 4 + 2 * karatsuba_lower_bound" by simp
    also have "...  8 * 2 ^ (l - 1) + 4 * 2 ^ (l - 1) + 2 * karatsuba_lower_bound" by simp
    also have "... = 12 * 2 ^ (l - 1) + 2 * karatsuba_lower_bound" by simp
    also have "... = 6 * 2 ^ l + 2 * karatsuba_lower_bound"
      using Suc_diff_1[OF l > 0, symmetric] power_Suc[of "2::nat" "l - 1"] by simp
    finally show ?thesis .
  qed
qed

text "The following is a pretty crude estimate for the length of the result of our Karatsuba
implementation, but it suffices for our purposes."

lemma length_karatsuba_on_power_of_2_length_le:
  assumes "k = 2 ^ l"
  assumes "length x = k" "length y = k"
  shows "length (karatsuba_on_power_of_2_length k x y)  6 * k + 2 * karatsuba_lower_bound"
  using order.trans[OF length_karatsuba_on_power_of_2_aux[OF assms] len_kar_bound_le]
  unfolding assms .

text "In order to multiply two integers of arbitrary length using Karatsuba multiplication, the
input numbers can just be zero-padded."

fun karatsuba_mul_nat :: "nat_lsbf  nat_lsbf  nat_lsbf" where
"karatsuba_mul_nat x y = (let k = next_power_of_2 (max (length x) (length y)) in
  karatsuba_on_power_of_2_length k (fill k x) (fill k y))"

text "We verify the correctness of Karatsuba multiplication:"

theorem karatsuba_mul_nat_correct: "to_nat (karatsuba_mul_nat x y) = to_nat x * to_nat y"
proof -
  define k where "k = next_power_of_2 (max (length x) (length y))"
  then obtain l where "k = 2 ^ l" using next_power_of_2_is_power_of_2 by blast
  have 1: "to_nat (fill k x) = to_nat x" "to_nat (fill k y) = to_nat y" by simp_all
  have "k  length x" "k  length y"
    using next_power_of_2_lower_bound[of "max (length x) (length y)"] k_def
    by simp_all
  hence "length (fill k x) = k" "length (fill k y) = k" using length_fill by simp_all
  show ?thesis unfolding k_def[symmetric] karatsuba_lower_bound_def
    using karatsuba_on_power_of_2_length_correct[OF k = 2 ^ l length (fill k x) = k length (fill k y) = k]
    by (simp only: karatsuba_mul_nat.simps Let_def k_def[symmetric] to_nat_fill)
qed

lemma length_karatsuba_mul_nat_le: "length (karatsuba_mul_nat x y)  12 * max (length x) (length y) + (6 + 2 * karatsuba_lower_bound)"
proof -
  let ?m = "max (length x) (length y)"
  define k where "k = next_power_of_2 ?m"
  then obtain l where "k = 2 ^ l" using next_power_of_2_is_power_of_2 by auto
  from k_def have "?m  k" using next_power_of_2_lower_bound by simp
  from k_def have "karatsuba_mul_nat x y = karatsuba_on_power_of_2_length k (fill k x) (fill k y)"
    unfolding karatsuba_mul_nat.simps Let_def by argo
  also have "length ...  6 * k + 2 * karatsuba_lower_bound"
    apply (intro length_karatsuba_on_power_of_2_length_le[OF k = 2 ^ l] length_fill)
    subgoal using ?m  k by simp
    subgoal using ?m  k by simp
    done
  also have "...  6 * (2 * ?m + 1) + 2 * karatsuba_lower_bound"
    apply (intro add_mono mult_le_mono order.refl)
    unfolding k_def by (rule next_power_of_2_upper_bound')
  also have "... = 12 * ?m + (6 + 2 * karatsuba_lower_bound)"
    by simp
  finally show ?thesis .
qed

text "Formally, we only implemented Karatsuba multiplication on natural numbers (not all integers).
However, this does not really matter, as the multiplication can just be lifted to the integers.
This lifting has already been done on other types, but for the sake of completeness we will just add
it here as well:"

fun karatsuba_mul_int where
"karatsuba_mul_int x y = nat_mul_to_int_mul karatsuba_mul_nat x y"

corollary karatsuba_mul_int_correct:
"to_int (karatsuba_mul_int x y) = to_int x * to_int y"
  using nat_mul_to_int_mul_correct[of karatsuba_mul_nat] karatsuba_mul_nat_correct
  by (metis karatsuba_mul_int.simps surj_pair)

end