Theory HOL-Library.Discrete

(* Author: Florian Haftmann, TU Muenchen *)

section Common discrete functions

theory Discrete
imports Complex_Main
begin

subsection Discrete logarithm

context
begin

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

lemma 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: 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 log_zero [simp]: "log 0 = 0"
  by (simp add: log.simps)

lemma log_one [simp]: "log 1 = 0"
  by (simp add: log.simps)

lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
  using log_one by simp

lemma log_rec: "n  2  log n = Suc (log (n div 2))"
  by (simp add: log.simps)

lemma log_twice [simp]: "n  0  log (2 * n) = Suc (log n)"
  by (simp add: log_rec)

lemma log_half [simp]: "log (n div 2) = 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: log_rec)
qed

lemma log_exp [simp]: "log (2 ^ n) = n"
  by (induct n) simp_all

lemma log_mono: "mono log"
proof
  fix m n :: nat
  assume "m  n"
  then show "log m  log n"
  proof (induct m arbitrary: n rule: log.induct)
    case (1 m)
    then have mn2: "m div 2  n div 2" by arith
    show "log m  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 "log (m div 2)  log (n div 2)" by blast
      with m2_0 n2_0 have "log (2 * (m div 2))  log (2 * (n div 2))" by simp
      with m2_0 n2_0 m  2 n  2 show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
    qed
  qed
qed

lemma log_exp2_le:
  assumes "n > 0"
  shows "2 ^ log n  n"
  using assms
proof (induct n rule: log_induct)
  case one
  then show ?case by simp
next
  case (double n)
  with log_mono have "log n  Suc 0"
    by (simp add: log.simps)
  assume "2 ^ log (n div 2)  n div 2"
  with n  2 have "2 ^ (log n - Suc 0)  n div 2" by simp
  then have "2 ^ (log n - Suc 0) * 2 ^ 1  n div 2 * 2" by simp
  with log n  Suc 0 have "2 ^ 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 log_exp2_gt: "2 * 2 ^ log n > n"
proof (cases "n > 0")
  case True
  thus ?thesis
  proof (induct n rule: log_induct)
    case (double n)
    thus ?case
      by (cases "even n") (auto elim!: evenE oddE simp: field_simps log.simps)
  qed simp_all
qed simp_all

lemma log_exp2_ge: "2 * 2 ^ log n  n"
  using log_exp2_gt[of n] by simp

lemma log_le_iff: "m  n  log m  log n"
  by (rule monoD [OF log_mono])

lemma log_eqI:
  assumes "n > 0" "2^k  n" "n < 2 * 2^k"
  shows   "log n = k"
proof (rule antisym)
  from n > 0 have "2 ^ log n  n" by (rule log_exp2_le)
  also have " < 2 ^ Suc k" using assms by simp
  finally have "log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all
  thus "log n  k" by simp
next
  have "2^k  n" by fact
  also have " < 2^(Suc (log n))" by (simp add: log_exp2_gt)
  finally have "k < Suc (log n)" by (subst (asm) power_strict_increasing_iff) simp_all
  thus "k  log n" by simp
qed

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


subsection Discrete square root

qualified definition sqrt :: "nat  nat"
  where "sqrt n = Max {m. m2  n}"

lemma sqrt_aux:
  fixes n :: nat
  shows "finite {m. m2  n}" and "{m. m2  n}  {}"
proof -
  { fix m
    assume "m2  n"
    then have "m  n"
      by (cases m) (simp_all add: power2_eq_square)
  } note ** = this
  then have "{m. m2  n}  {m. m  n}" by auto
  then show "finite {m. m2  n}" by (rule finite_subset) rule
  have "02  n" by simp
  then show *: "{m. m2  n}  {}" by blast
qed

lemma sqrt_unique:
  assumes "m^2  n" "n < (Suc m)^2"
  shows   "Discrete.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 sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def
    by (intro antisym Max.boundedI Max.coboundedI) simp_all
qed


lemma sqrt_code[code]: "sqrt n = Max (Set.filter (λm. m2  n) {0..n})"
proof -
  from power2_nat_le_imp_le [of _ n] have "{m. m  n  m2  n} = {m. m2  n}" by auto
  then show ?thesis by (simp add: sqrt_def Set.filter_def)
qed

lemma sqrt_inverse_power2 [simp]: "sqrt (n2) = n"
proof -
  have "{m. m  n}  {}" by auto
  then have "Max {m. m  n}  n" by auto
  then show ?thesis
    by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
qed

lemma sqrt_zero [simp]: "sqrt 0 = 0"
  using sqrt_inverse_power2 [of 0] by simp

lemma sqrt_one [simp]: "sqrt 1 = 1"
  using sqrt_inverse_power2 [of 1] by simp

lemma mono_sqrt: "mono sqrt"
proof
  fix m n :: nat
  have *: "0 * 0  m" by simp
  assume "m  n"
  then show "sqrt m  sqrt n"
    by (auto intro!: Max_mono 0 * 0  m finite_less_ub simp add: power2_eq_square sqrt_def)
qed

lemma mono_sqrt': "m  n  Discrete.sqrt m  Discrete.sqrt n"
  using mono_sqrt unfolding mono_def by auto

lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0  n > 0"
proof -
  have *: "0 < Max {m. m2  n}  (a{m. m2  n}. 0 < a)"
    by (rule Max_gr_iff) (fact sqrt_aux)+
  show ?thesis
  proof
    assume "0 < sqrt n"
    then have "0 < Max {m. m2  n}" by (simp add: sqrt_def)
    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
  next
    assume "0 < n"
    then have "12  n  0 < (1::nat)" by simp
    then have "q. q2  n  0 < q" ..
    with * have "0 < Max {m. m2  n}" by blast
    then show "0 < sqrt n" by  (simp add: sqrt_def)
  qed
qed

lemma sqrt_power2_le [simp]: "(sqrt n)2  n" (* FIXME tune proof *)
proof (cases "n > 0")
  case False then show ?thesis by simp
next
  case True then have "sqrt n > 0" by simp
  then have "mono (times (Max {m. m2  n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
  then have *: "Max {m. m2  n} * Max {m. m2  n} = Max (times (Max {m. m2  n}) ` {m. m2  n})"
    using 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 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: sqrt_def power2_eq_square)
qed

lemma sqrt_le: "sqrt n  n"
  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)

text Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl
  
lemma Suc_sqrt_power2_gt: "n < (Suc (Discrete.sqrt n))^2"
  using Max_ge[OF Discrete.sqrt_aux(1), of "Discrete.sqrt n + 1" n]
  by (cases "n < (Suc (Discrete.sqrt n))^2") (simp_all add: Discrete.sqrt_def)

lemma le_sqrt_iff: "x  Discrete.sqrt y  x^2  y"
proof -
  have "x  Discrete.sqrt y  (z. z2  y  x  z)"    
    using Max_ge_iff[OF Discrete.sqrt_aux, of x y] by (simp add: Discrete.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_sqrtI: "x^2  y  x  Discrete.sqrt y"
  by (simp add: le_sqrt_iff)

lemma sqrt_le_iff: "Discrete.sqrt y  x  (z. z^2  y  z  x)"
  using Max.bounded_iff[OF Discrete.sqrt_aux] by (simp add: Discrete.sqrt_def)

lemma sqrt_leI:
  "(z. z^2  y  z  x)  Discrete.sqrt y  x"
  by (simp add: sqrt_le_iff)
    
lemma sqrt_Suc:
  "Discrete.sqrt (Suc n) = (if m. Suc n = m^2 then Suc (Discrete.sqrt n) else Discrete.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: "Discrete.sqrt (Suc n) = m" by simp
  from m_def sqrt_power2_le[of n] 
    have "(Discrete.sqrt n)^2 < m^2" by linarith
  with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
  from m_def Suc_sqrt_power2_gt[of "n"]
    have "m^2  (Suc(Discrete.sqrt n))^2"
      by linarith
  with power2_nat_le_eq_le have "m  Suc (Discrete.sqrt n)" by blast
  with lt_m have "m = Suc (Discrete.sqrt n)" by simp
  with lhs m_def show ?thesis by fastforce
next
  assume asm: "¬ ( m. Suc n = m^2)"
  hence "Suc n  (Discrete.sqrt (Suc n))^2" by simp
  with sqrt_power2_le[of "Suc n"] 
    have "Discrete.sqrt (Suc n)  Discrete.sqrt n" by (intro le_sqrtI) linarith
  moreover have "Discrete.sqrt (Suc n)  Discrete.sqrt n"
    by (intro monoD[OF mono_sqrt]) simp_all
  ultimately show ?thesis using asm by simp
qed

end

end