Theory Discrete

theory Discrete
imports Main
(* Author: Florian Haftmann, TU Muenchen *)

section ‹Common discrete functions›

theory Discrete
imports 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
    moreover with * have "P (n div 2)" .
    ultimately 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)
  show "2 ^ log 1 ≤ (1 :: nat)" by simp
next
  fix n :: nat
  assume "n ≥ 2"
  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 "2 ^ log n ≤ n" .
qed


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 [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 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 "Max (op * (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 simp
    apply (metis le0 mult_0_right)
    apply auto
    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)
        then show ?thesis
          apply simp
          apply (subst Max_le_iff)
          apply auto
          apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
          apply (metis ‹q * q ≤ n›)
          apply (metis ‹q * q ≤ n› le_cases mult_le_mono1 mult_le_mono2 order_trans)
          done
      qed
    qed
  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)

end

end