Quelle  Discrete_Functions.thy   Sprache: Isabelle

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Common discrete functions›

theory Discrete_Functions
imports Complex_Main
begin

subsection ‹Discrete logarithm›

fun floor_log :: "nat \ nat"
  where [simp del]: "floor_log n = (if n < 2 then 0 else Suc (floor_log (n div 2)))"

lemma floor_log_induct [consumes 1, case_names one double]:
  fixes n :: nat
  assumes "n > 0"
  assumes one: "P 1"
  assumes double: "\n. n \ 2 \ P (n div 2) \ P n"
  shows "P n"
using ‹n > 0› proof (induct n rule: floor_log.induct)
  fix n
  assume "\ n < 2 \
          0 < n div 2 ==> P (n div 2)"
  then have *: "n \ 2 \ P (n div 2)" by simp
  assume "n > 0"
  show "P n"
  proof (cases "n = 1")
    case True
    with one show ?thesis by simp
  next
    case False
    with ‹n > 0› have "n \ 2" by auto
    with * have "P (n div 2)" .
    with ‹n ≥ 2› show ?thesis by (rule double)
  qed
qed

lemma floor_log_zero [simp]: "floor_log 0 = 0"
  by (simp add: floor_log.simps)

lemma floor_log_one [simp]: "floor_log 1 = 0"
  by (simp add: floor_log.simps)

lemma floor_log_Suc_zero [simp]: "floor_log (Suc 0) = 0"
  using floor_log_one by simp

lemma floor_log_rec: "n \ 2 \ floor_log n = Suc (floor_log (n div 2))"
  by (simp add: floor_log.simps)

lemma floor_log_twice [simp]: "n \ 0 \ floor_log (2 * n) = Suc (floor_log n)"
  by (simp add: floor_log_rec)

lemma floor_log_half [simp]: "floor_log (n div 2) = floor_log n - 1"
proof (cases "n < 2")
  case True
  then have "n = 0 \ n = 1" by arith
  then show ?thesis by (auto simp del: One_nat_def)
next
  case False
  then show ?thesis by (simp add: floor_log_rec)
qed

lemma floor_log_power [simp]: "floor_log (2 ^ n) = n"
  by (induct n) simp_all

lemma floor_log_mono: "mono floor_log"
proof
  fix m n :: nat
  assume "m \ n"
  then show "floor_log m \ floor_log n"
  proof (induct m arbitrary: n rule: floor_log.induct)
    case (1 m)
    then have mn2: "m div 2 \ n div 2" by arith
    show "floor_log m \ floor_log n"
    proof (cases "m \ 2")
      case False
      then have "m = 0 \ m = 1" by arith
      then show ?thesis by (auto simp del: One_nat_def)
    next
      case True then have "\ m < 2" by simp
      with mn2 have "n \ 2" by arith
      from True have m2_0: "m div 2 \ 0" by arith
      with mn2 have n2_0: "n div 2 \ 0" by arith
      from ‹¬ m < 2› "1.hyps" mn2 have "floor_log (m div 2) \ floor_log (n div 2)" by blast
      with m2_0 n2_0 have "floor_log (2 * (m div 2)) \ floor_log (2 * (n div 2))" by simp
      with m2_0 n2_0 ‹m ≥ 2› ‹n ≥ 2› show ?thesis by (simp only: floor_log_rec [of m] floor_log_rec [of n]) simp
    qed
  qed
qed

lemma floor_log_exp2_le:
  assumes "n > 0"
  shows "2 ^ floor_log n \ n"
  using assms
proof (induct n rule: floor_log_induct)
  case one
  then show ?case by simp
next
  case (double n)
  with floor_log_mono have "floor_log n \ Suc 0"
    by (simp add: floor_log.simps)
  assume "2 ^ floor_log (n div 2) \ n div 2"
  with ‹n ≥ 2› have "2 ^ (floor_log n - Suc 0) \ n div 2" by simp
  then have "2 ^ (floor_log n - Suc 0) * 2 ^ 1 \ n div 2 * 2" by simp
  with ‹floor_log n ≥ Suc 0› have "2 ^ floor_log n \ n div 2 * 2"
    unfolding power_add [symmetric] by simp
  also have "n div 2 * 2 \ n" by (cases "even n") simp_all
  finally show ?case .
qed

lemma floor_log_exp2_gt: "2 * 2 ^ floor_log n > n"
proof (cases "n > 0")
  case True
  thus ?thesis
  proof (induct n rule: floor_log_induct)
    case (double n)
    thus ?case
      by (cases "even n") (auto elim!: evenE oddE simp: field_simps floor_log.simps)
  qed simp_all
qed simp_all

lemma floor_log_exp2_ge: "2 * 2 ^ floor_log n \ n"
  using floor_log_exp2_gt[of n] by simp

lemma floor_log_le_iff: "m \ n \ floor_log m \ floor_log n"
  by (rule monoD [OF floor_log_mono])

lemma floor_log_eqI:
  assumes "n > 0" "2^k \ n" "n < 2 * 2^k"
  shows   "floor_log n = k"
proof (rule antisym)
  from ‹n > 0› have "2 ^ floor_log n \ n" by (rule floor_log_exp2_le)
  also have "\ < 2 ^ Suc k" using assms by simp
  finally have "floor_log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all
  thus "floor_log n \ k" by simp
next
  have "2^k \ n" by fact
  also have "\ < 2^(Suc (floor_log n))" by (simp add: floor_log_exp2_gt)
  finally have "k < Suc (floor_log n)" by (subst (asm) power_strict_increasing_iff) simp_all
  thus "k \ floor_log n" by simp
qed

lemma floor_log_altdef: "floor_log n = (if n = 0 then 0 else nat \log 2 (real_of_nat n)\)"
proof (cases "n = 0")
  case False
  have "\log 2 (real_of_nat n)\ = int (floor_log n)"
  proof (rule floor_unique)
    from False have "2 powr (real (floor_log n)) \ real n"
      by (simp add: powr_realpow floor_log_exp2_le)
    hence "log 2 (2 powr (real (floor_log n))) \ log 2 (real n)"
      using False by (subst log_le_cancel_iff) simp_all
    also have "log 2 (2 powr (real (floor_log n))) = real (floor_log n)" by simp
    finally show "real_of_int (int (floor_log n)) \ log 2 (real n)" by simp
  next
    have "real n < real (2 * 2 ^ floor_log n)"
      by (subst of_nat_less_iff) (rule floor_log_exp2_gt)
    also have "\ = 2 powr (real (floor_log n) + 1)"
      by (simp add: powr_add powr_realpow)
    finally have "log 2 (real n) < log 2 \"
      using False by (subst log_less_cancel_iff) simp_all
    also have "\ = real (floor_log n) + 1" by simp
    finally show "log 2 (real n) < real_of_int (int (floor_log n)) + 1" by simp
  qed
  thus ?thesis by simp
qed simp_all


subsection ‹Discrete square root›

definition floor_sqrt :: "nat \ nat"
  where "floor_sqrt n = Max {m. m\<^sup>2 \ n}"

lemma floor_sqrt_aux:
  fixes n :: nat
  shows "finite {m. m\<^sup>2 \ n}" and "{m. m\<^sup>2 \ n} \ {}"
proof -
  have **: "m \ n" if "m\<^sup>2 \ n" for m
    using that by (cases m) (simp_all add: power2_eq_square)
  then have "{m. m\<^sup>2 \ n} \ {m. m \ n}" by auto
  then show "finite {m. m\<^sup>2 \ n}" by (rule finite_subset) rule
  have "0\<^sup>2 \ n" by simp
  then show *: "{m. m\<^sup>2 \ n} \ {}" by blast
qed

lemma floor_sqrt_unique:
  assumes "m^2 \ n" "n < (Suc m)^2"
  shows   "floor_sqrt n = m"
proof -
  have "m' \ m" if "m'^2 \ n" for m'
  proof -
    note that
    also note assms(2)
    finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all
    thus "m' \ m" by simp
  qed
  with ‹m^2 ≤ n› floor_sqrt_aux[of n] show ?thesis unfolding floor_sqrt_def
    by (intro antisym Max.boundedI Max.coboundedI) simp_all
qed

lemma floor_sqrt_inverse_power2 [simp]: "floor_sqrt (n\<^sup>2) = n"
proof -
  have "{m. m \ n} \ {}" by auto
  then have "Max {m. m \ n} \ n" by auto
  then show ?thesis
    by (auto simp add: floor_sqrt_def power2_nat_le_eq_le intro: antisym)
qed

lemma floor_sqrt_zero [simp]: "floor_sqrt 0 = 0"
  using floor_sqrt_inverse_power2 [of 0] by simp

lemma floor_sqrt_one [simp]: "floor_sqrt 1 = 1"
  using floor_sqrt_inverse_power2 [of 1] by simp

lemma floor_sqrt_Suc_0 [simp]:
  ‹floor_sqrt (Suc 0) = 1›
  using floor_sqrt_inverse_power2 [of 1] by simp

lemma mono_floor_sqrt: "mono floor_sqrt"
proof
  fix m n :: nat
  have *: "0 * 0 \ m" by simp
  assume "m \ n"
  then show "floor_sqrt m \ floor_sqrt n"
    by (auto intro!: Max_mono ‹0 * 0 ≤ m› finite_less_ub simp add: power2_eq_square floor_sqrt_def)
qed

lemma mono_floor_sqrt': "m \ n \ floor_sqrt m \ floor_sqrt n"
  using mono_floor_sqrt unfolding mono_def by auto

lemma floor_sqrt_greater_zero_iff [simp]: "floor_sqrt n > 0 \ n > 0"
proof -
  have *: "0 < Max {m. m\<^sup>2 \ n} \ (\a\{m. m\<^sup>2 \ n}. 0 < a)"
    by (rule Max_gr_iff) (fact floor_sqrt_aux)+
  show ?thesis
  proof
    assume "0 < floor_sqrt n"
    then have "0 < Max {m. m\<^sup>2 \ n}" by (simp add: floor_sqrt_def)
    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
  next
    assume "0 < n"
    then have "1\<^sup>2 \ n \ 0 < (1::nat)" by simp
    then have "\q. q\<^sup>2 \ n \ 0 < q" ..
    with * have "0 < Max {m. m\<^sup>2 \ n}" by blast
    then show "0 < floor_sqrt n" by  (simp add: floor_sqrt_def)
  qed
qed

lemma floor_sqrt_power2_le [simp]: "(floor_sqrt n)\<^sup>2 \ n" (* FIXME tune proof *)
proof (cases "n > 0")
  case False then show ?thesis by simp
next
  case True then have "floor_sqrt n > 0" by simp
  then have "mono (times (Max {m. m\<^sup>2 \ n}))" by (auto intro: mono_times_nat simp add: floor_sqrt_def)
  then have *: "Max {m. m\<^sup>2 \ n} * Max {m. m\<^sup>2 \ n} = Max (times (Max {m. m\<^sup>2 \ n}) ` {m. m\<^sup>2 \ n})"
    using floor_sqrt_aux [of n] by (rule mono_Max_commute)
  have "\a. a * a \ n \ Max {m. m * m \ n} * a \ n"
  proof -
    fix q
    assume "q * q \ n"
    show "Max {m. m * m \ n} * q \ n"
    proof (cases "q > 0")
      case False then show ?thesis by simp
    next
      case True then have "mono (times q)" by (rule mono_times_nat)
      then have "q * Max {m. m * m \ n} = Max (times q ` {m. m * m \ n})"
        using floor_sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
      then have "Max {m. m * m \ n} * q = Max (times q ` {m. m * m \ n})" by (simp add: ac_simps)
      moreover have "finite ((*) q ` {m. m * m \ n})"
        by (metis (mono_tags) finite_imageI finite_less_ub le_square)
      moreover have "\x. x * x \ n"
        by (metis ‹q * q ≤ n›)
      ultimately show ?thesis
        by simp (metis ‹q * q ≤ n› le_cases mult_le_mono1 mult_le_mono2 order_trans)
    qed
  qed
  then have "Max ((*) (Max {m. m * m \ n}) ` {m. m * m \ n}) \ n"
    apply (subst Max_le_iff)
      apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
     apply auto
    apply (metis le0 mult_0_right)
    done
  with * show ?thesis by (simp add: floor_sqrt_def power2_eq_square)
qed

lemma floor_sqrt_le: "floor_sqrt n \ n"
  using floor_sqrt_aux [of n] by (auto simp add: floor_sqrt_def intro: power2_nat_le_imp_le)

text ‹Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl›

lemma Suc_floor_sqrt_power2_gt: "n < (Suc (floor_sqrt n))^2"
  using Max_ge[OF floor_sqrt_aux(1), of "floor_sqrt n + 1" n]
  by (cases "n < (Suc (floor_sqrt n))^2") (simp_all add: floor_sqrt_def)

lemma le_floor_sqrt_iff: "x \ floor_sqrt y \ x^2 \ y"
proof -
  have "x \ floor_sqrt y \ (\z. z\<^sup>2 \ y \ x \ z)"
    using Max_ge_iff[OF floor_sqrt_aux, of x y] by (simp add: floor_sqrt_def)
  also have "\ \ x^2 \ y"
  proof safe
    fix z assume "x \ z" "z ^ 2 \ y"
    thus "x^2 \ y" by (intro le_trans[of "x^2" "z^2" y]) (simp_all add: power2_nat_le_eq_le)
  qed auto
  finally show ?thesis .
qed

lemma le_floor_sqrtI: "x^2 \ y \ x \ floor_sqrt y"
  by (simp add: le_floor_sqrt_iff)

lemma floor_sqrt_le_iff:
  ‹floor_sqrt y ≤ x ⟷ (∀z. z🚫2 ≤ y ⟶ z ≤ x)›
  using Max.bounded_iff [OF floor_sqrt_aux]
  by (simp add: floor_sqrt_def)

lemma floor_sqrt_leI:
  "(\z. z^2 \ y \ z \ x) \ floor_sqrt y \ x"
  by (simp add: floor_sqrt_le_iff)

lemma floor_sqrt_less_eq_half:
  ‹floor_sqrt n ≤ Suc n div 2›
proof (rule floor_sqrt_leI)
  fix m
  assume ‹m🚫2 ≤ n›
  have ‹m < Suc (Suc n div 2)›
  proof (rule ccontr, unfold not_less)
    assume ‹Suc (Suc n div 2) ≤ m›
    then have ‹(Suc (Suc n div 2))🚫2 ≤ m🚫2›
      by simp
    then have ‹(Suc (Suc n div 2))🚫2 ≤ n›
      using ‹m🚫2 ≤ n› by (rule order_trans)
    then show False
      by (simp only: Suc_eq_plus1 power2_sum algebra_simps) auto
  qed
  then show ‹m ≤ Suc n div 2›
    by simp
qed

lemma floor_sqrt_Suc:
  "floor_sqrt (Suc n) = (if \m. Suc n = m^2 then Suc (floor_sqrt n) else floor_sqrt n)"
proof cases
  assume "\ m. Suc n = m^2"
  then obtain m where m_def: "Suc n = m^2" by blast
  then have lhs: "floor_sqrt (Suc n) = m" by simp
  from m_def floor_sqrt_power2_le[of n]
    have "(floor_sqrt n)^2 < m^2" by linarith
  with power2_less_imp_less have lt_m: "floor_sqrt n < m" by blast
  from m_def Suc_floor_sqrt_power2_gt[of "n"]
    have "m^2 \ (Suc(floor_sqrt n))^2"
      by linarith
  with power2_nat_le_eq_le have "m \ Suc (floor_sqrt n)" by blast
  with lt_m have "m = Suc (floor_sqrt n)" by simp
  with lhs m_def show ?thesis by fastforce
next
  assume asm: "\ (\ m. Suc n = m^2)"
  hence "Suc n \ (floor_sqrt (Suc n))^2" by simp
  with floor_sqrt_power2_le[of "Suc n"]
    have "floor_sqrt (Suc n) \ floor_sqrt n" by (intro le_floor_sqrtI) linarith
  moreover have "floor_sqrt (Suc n) \ floor_sqrt n"
    by (intro monoD[OF mono_floor_sqrt]) simp_all
  ultimately show ?thesis using asm by simp
qed

text ‹Computation by divide and conquer›

definition floor_sqrt_between :: ‹nat ==> nat ==> nat ==> nat›
  where floor_sqrt_between_eq:
    ‹floor_sqrt_between m q n =
      (if floor_sqrt n ∈ {m..<m + q} then floor_sqrt n else 0)›
    🍋‹
      The 🍋‹0::nat› is not for relevant regular computation
      and can be chosen arbitrarily.
    ›

lemma floor_sqrt_between_out_of_bounds:
  ‹floor_sqrt_between m 0 n = 0›
  by (simp add: floor_sqrt_between_eq)

lemma floor_sqrt_between_singleton:
  ‹floor_sqrt_between m (Suc 0) n =
    (if m🚫2 ≤ n ∧ n < (Suc m)🚫2 then m else 0)›
  by (auto simp add: floor_sqrt_between_eq Suc_floor_sqrt_power2_gt floor_sqrt_unique)

lemma floor_sqrt_between_rec:
  ‹floor_sqrt_between m q n = (
    let
      r = q div 2;
      p = m + r;
      s = p🚫2
    in
      if s = n
      then p
      else if s < n
        then floor_sqrt_between (m + r) (q - r) n
        else floor_sqrt_between m r n
  )› if ‹q > 0›
  using that le_floor_sqrt_iff [of ‹m + q div 2› n]
  by (auto simp add: floor_sqrt_between_eq Let_def not_less)

lemma floor_sqrt_between_code [code]:
  ‹floor_sqrt_between m q n = (
    if q = 0 then 0
    else if q = 1
    then if m🚫2 ≤ n ∧ n < (Suc m)🚫2
      then m
      else 0
    else
      let
        r = q div 2;
        p = m + r;
        s = p🚫2
      in
        if s = n
        then p
        else if s < n
          then floor_sqrt_between (m + r) (q - r) n
          else floor_sqrt_between m r n
  )›
proof -
  consider ‹q = 0› | ‹q = 1› | ‹q ≥ 2›
    by (cases ‹q ≥ 2›; cases q) simp_all
  then show ?thesis
    by cases
      (simp_all add: floor_sqrt_between_out_of_bounds floor_sqrt_between_singleton floor_sqrt_between_rec)
qed

lemma [code]:
  ‹floor_sqrt n = floor_sqrt_between 0 (Suc (Suc n div 2)) n›
  using floor_sqrt_less_eq_half [of n] by (simp add: floor_sqrt_between_eq)

end