diff -r 07c802837a8c -r da3bf4a755b3 src/HOL/Library/Log_Nat.thy
--- a/src/HOL/Library/Log_Nat.thy	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/HOL/Library/Log_Nat.thy	Wed Nov 13 15:00:17 2024 +0000
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Library/Log_Nat.thy
-    Author:     Johannes Hölzl, Fabian Immler
+    Author:     Johannes Hölzl, Fabian Immler, Manuel Eberl
     Copyright   2012  TU München
 *)
 
@@ -199,6 +199,183 @@
 qed
 
 
+subsection \<open>\<close>
+
+
+definition ceillog2 :: "nat \<Rightarrow> nat" where
+  "ceillog2 n = (if n = 0 then 0 else nat \<lceil>log 2 (real n)\<rceil>)"
+
+lemma ceillog2_0 [simp]: "ceillog2 0 = 0"
+  and ceillog2_Suc_0 [simp]: "ceillog2 (Suc 0) = 0"
+  and ceillog2_2 [simp]: "ceillog2 2 = 1"
+  by (auto simp: ceillog2_def)
+
+lemma ceillog2_le1_eq_0 [simp]: "n \<le> 1 \<Longrightarrow> ceillog2 n = 0"
+  by (cases n) auto
+
+lemma ceillog2_2_power [simp]: "ceillog2 (2 ^ n) = n"
+  by (auto simp: ceillog2_def)
+
+lemma ceillog2_ge_log:
+  assumes "n > 0"
+  shows   "real (ceillog2 n) \<ge> log 2 (real n)"
+proof -
+  have "real_of_int \<lceil>log 2 (real n)\<rceil> \<ge> log 2 (real n)"
+    by linarith
+  thus ?thesis
+    using assms unfolding ceillog2_def by auto
+qed
+
+lemma ceillog2_less_log:
+  assumes "n > 0"
+  shows   "real (ceillog2 n) < log 2 (real n) + 1"
+proof -
+  have "real_of_int \<lceil>log 2 (real n)\<rceil> < log 2 (real n) + 1"
+    by linarith
+  thus ?thesis
+    using assms unfolding ceillog2_def by auto
+qed
+
+lemma ceillog2_le_iff:
+  assumes "n > 0"
+  shows   "ceillog2 n \<le> l \<longleftrightarrow> n \<le> 2 ^ l"
+proof -
+  have "ceillog2 n \<le> l \<longleftrightarrow> real n \<le> 2 ^ l"
+    unfolding ceillog2_def using assms by (auto simp: log_le_iff powr_realpow)
+  also have "2 ^ l = real (2 ^ l)"
+    by simp
+  also have "real n \<le> real (2 ^ l) \<longleftrightarrow> n \<le> 2 ^ l"
+    by linarith
+  finally show ?thesis .
+qed
+
+lemma ceillog2_ge_iff:
+  assumes "n > 0"
+  shows   "ceillog2 n \<ge> l \<longleftrightarrow> 2 ^ l < 2 * n"
+proof -
+  have "-1 < (0 :: real)"
+    by auto
+  also have "\<dots> \<le> log 2 (real n)"
+    using assms by auto
+  finally have "ceillog2 n \<ge> l \<longleftrightarrow> real l - 1 < log 2 (real n)"
+    unfolding ceillog2_def using assms by (auto simp: le_nat_iff le_ceiling_iff)
+  also have "\<dots> \<longleftrightarrow> real l < log 2 (real (2 * n))"
+    using assms by (auto simp: log_mult)
+  also have "\<dots> \<longleftrightarrow> 2 ^ l < real (2 * n)"
+    using assms by (subst less_log_iff) (auto simp: powr_realpow)
+  also have "2 ^ l = real (2 ^ l)"
+    by simp
+  also have "real (2 ^ l) < real (2 * n) \<longleftrightarrow> 2 ^ l < 2 * n"
+    by linarith
+  finally show ?thesis .
+qed
+
+lemma le_two_power_ceillog2: "n \<le> 2 ^ ceillog2 n"
+  using neq0_conv ceillog2_le_iff by blast
+
+lemma two_power_ceillog2_gt:
+  assumes "n > 0"
+  shows   "2 * n > 2 ^ ceillog2 n"
+  using ceillog2_ge_iff[of n "ceillog2 n"] assms by simp
+
+lemma ceillog2_eqI:
+  assumes "n \<le> 2 ^ l" "2 ^ l < 2 * n"
+  shows   "ceillog2 n = l"
+  by (metis Suc_leI assms bot_nat_0.not_eq_extremum ceillog2_ge_iff ceillog2_le_iff le_antisym mult_is_0
+      not_less_eq_eq)
+
+lemma ceillog2_rec_even:
+  assumes "k > 0"
+  shows   "ceillog2 (2 * k) = Suc (ceillog2 k)"
+  by (rule ceillog2_eqI) (auto simp: le_two_power_ceillog2 two_power_ceillog2_gt assms)
+
+lemma ceillog2_mono:
+  assumes "m \<le> n"
+  shows   "ceillog2 m \<le> ceillog2 n"
+proof (cases "m = 0")
+  case False
+  have "\<lceil>log 2 (real m)\<rceil> \<le> \<lceil>log 2 (real n)\<rceil>"
+    by (intro ceiling_mono) (use False assms in auto)
+  hence "nat \<lceil>log 2 (real m)\<rceil> \<le> nat \<lceil>log 2 (real n)\<rceil>"
+    by linarith
+  thus ?thesis using False assms
+    unfolding ceillog2_def by simp
+qed auto
+  
+lemma ceillog2_rec_odd:
+  assumes "k > 0"
+  shows   "ceillog2 (Suc (2 * k)) = Suc (ceillog2 (Suc k))"
+proof -
+  have "2 ^ ceillog2 (Suc (2 * k)) > Suc (2 * k)"
+    by (metis assms diff_Suc_1 dvd_triv_left le_two_power_ceillog2 mult_pos_pos nat_power_eq_Suc_0_iff 
+        order_less_le pos2 semiring_parity_class.even_mask_iff)
+  then have "ceillog2 (2 * k + 2) \<le> ceillog2 (2 * k + 1)"
+    by (simp add: ceillog2_le_iff)
+  moreover have "ceillog2 (2 * k + 2) \<ge> ceillog2 (2 * k + 1)"
+    by (rule ceillog2_mono) auto
+  ultimately have "ceillog2 (2 * k + 2) = ceillog2 (2 * k + 1)"
+    by (rule antisym)
+  also have "2 * k + 2 = 2 * Suc k"
+    by simp
+  also have "ceillog2 (2 * Suc k) = Suc (ceillog2 (Suc k))"
+    by (rule ceillog2_rec_even) auto
+  finally show ?thesis 
+    by simp
+qed  
+
+(* TODO: better code is possible using bitlen and "count trailing 0 bits" *)
+lemma ceillog2_rec:
+  "ceillog2 n = (if n \<le> 1 then 0 else 1 + ceillog2 ((n + 1) div 2))"
+proof (cases "n \<le> 1")
+  case True
+  thus ?thesis
+    by (cases n) auto
+next
+  case False
+  thus ?thesis
+    by (cases "even n") (auto elim!: evenE oddE simp: ceillog2_rec_even ceillog2_rec_odd)
+qed
+
+lemma funpow_div2_ceillog2_le_1:
+  "((\<lambda>n. (n + 1) div 2) ^^ ceillog2 n) n \<le> 1"
+proof (induction n rule: less_induct)
+  case (less n)
+  show ?case
+  proof (cases "n \<le> 1")
+    case True
+    thus ?thesis by (cases n) auto
+  next
+    case False
+    have "((\<lambda>n. (n + 1) div 2) ^^ Suc (ceillog2 ((n + 1) div 2))) n \<le> 1"
+      using less.IH[of "(n+1) div 2"] False by (subst funpow_Suc_right) auto
+    also have "Suc (ceillog2 ((n + 1) div 2)) = ceillog2 n"
+      using False by (subst ceillog2_rec[of n]) auto
+    finally show ?thesis .
+  qed
+qed
+
+
+fun ceillog2_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat" where 
+  "ceillog2_aux acc n = (if n \<le> 1 then acc else ceillog2_aux (acc + 1) ((n + 1) div 2))"
+
+lemmas [simp del] = ceillog2_aux.simps
+
+lemma ceillog2_aux_correct: "ceillog2_aux acc n = ceillog2 n + acc"
+proof (induction acc n rule: ceillog2_aux.induct)
+  case (1 acc n)
+  show ?case
+  proof (cases "n \<le> 1")
+    case False
+    thus ?thesis using ceillog2_rec[of n] "1.IH"
+      by (auto simp: ceillog2_aux.simps[of acc n])
+  qed (auto simp: ceillog2_aux.simps[of acc n])
+qed
+
+(* TODO: better code equation using bit operations *)
+lemma ceillog2_code [code]: "ceillog2 n = ceillog2_aux 0 n"
+  by (simp add: ceillog2_aux_correct)
+
+
 subsection \<open>Bitlen\<close>
 
 definition bitlen :: "int \<Rightarrow> int"