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. m² ≤ n}" lemma sqrt_aux: fixes n :: nat shows "finite {m. m² ≤ n}" and "{m. m² ≤ n} ≠ {}" proof - { fix m assume "m² ≤ n" then have "m ≤ n" by (cases m) (simp_all add: power2_eq_square) } note ** = this then have "{m. m² ≤ n} ⊆ {m. m ≤ n}" by auto then show "finite {m. m² ≤ n}" by (rule finite_subset) rule have "0² ≤ n" by simp then show *: "{m. m² ≤ 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. m² ≤ n) {0..n})" proof - from power2_nat_le_imp_le [of _ n] have "{m. m ≤ n ∧ m² ≤ n} = {m. m² ≤ n}" by auto then show ?thesis by (simp add: sqrt_def Set.filter_def) qed lemma sqrt_inverse_power2 [simp]: "sqrt (n²) = 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. m² ≤ n} ⟷ (∃a∈{m. m² ≤ n}. 0 < a)" by (rule Max_gr_iff) (fact sqrt_aux)+ show ?thesis proof assume "0 < sqrt n" then have "0 < Max {m. m² ≤ n}" by (simp add: sqrt_def) with * show "0 < n" by (auto dest: power2_nat_le_imp_le) next assume "0 < n" then have "1² ≤ n ∧ 0 < (1::nat)" by simp then have "∃q. q² ≤ n ∧ 0 < q" .. with * have "0 < Max {m. m² ≤ n}" by blast then show "0 < sqrt n" by (simp add: sqrt_def) qed qed lemma sqrt_power2_le [simp]: "(sqrt n)² ≤ 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. m² ≤ n}))" by (auto intro: mono_times_nat simp add: sqrt_def) then have *: "Max {m. m² ≤ n} * Max {m. m² ≤ n} = Max (times (Max {m. m² ≤ n}) ` {m. m² ≤ 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. z² ≤ 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