# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737454625 -3600
# Node ID 9a85d296ab813bf9ee3a4b6b0bda617ccca6356e
# Parent  88060e644af71b470658fb9549858e9150a90f4a# Parent  2828fdd15313fc64093c6ae844ccfb7ecade55df
merged

diff -r 88060e644af7 -r 9a85d296ab81 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Tue Jan 21 11:15:34 2025 +0100
+++ b/src/HOL/Bit_Operations.thy	Tue Jan 21 11:17:05 2025 +0100
@@ -132,6 +132,17 @@
   using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
   by simp (metis (full_types) add.left_commute add_left_imp_eq)
 
+lemma half_numeral_Bit1_eq [simp]:
+  \<open>numeral (num.Bit1 m) div 2 = numeral (num.Bit0 m) div 2\<close>
+  using even_half_succ_eq [of \<open>2 * numeral m\<close>]
+  by simp
+
+lemma double_half_numeral_Bit_0_eq [simp]:
+  \<open>2 * (numeral (num.Bit0 m) div 2) = numeral (num.Bit0 m)\<close>
+  \<open>(numeral (num.Bit0 m) div 2) * 2 = numeral (num.Bit0 m)\<close>
+  using mod_mult_div_eq [of \<open>numeral (Num.Bit0 m)\<close> 2]
+  by (simp_all add: mod2_eq_if ac_simps)
+
 named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
 
 definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
@@ -1195,7 +1206,7 @@
     by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff)
 qed
 
-lemma set_bit_0 [simp]:
+lemma set_bit_0:
   \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
 
@@ -1204,7 +1215,7 @@
   by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
     elim: possible_bit_less_imp)
 
-lemma unset_bit_0 [simp]:
+lemma unset_bit_0:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc)
 
@@ -1212,7 +1223,7 @@
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
 
-lemma flip_bit_0 [simp]:
+lemma flip_bit_0:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
 
@@ -1557,7 +1568,7 @@
 
 lemma drop_bit_Suc_bit1 [simp]:
   \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
 
 lemma drop_bit_numeral_bit0 [simp]:
   \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
@@ -1565,7 +1576,7 @@
 
 lemma drop_bit_numeral_bit1 [simp]:
   \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit1_div_2)
+  by (simp add: drop_bit_rec numeral_Bit0_div_2)
 
 lemma take_bit_Suc_1 [simp]:
   \<open>take_bit (Suc n) 1 = 1\<close>
@@ -1577,7 +1588,7 @@
 
 lemma take_bit_Suc_bit1:
   \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
+  by (simp add: take_bit_Suc numeral_Bit0_div_2 mod_2_eq_odd)
 
 lemma take_bit_numeral_1 [simp]:
   \<open>take_bit (numeral l) 1 = 1\<close>
@@ -1589,7 +1600,7 @@
 
 lemma take_bit_numeral_bit1:
   \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
+  by (simp add: take_bit_rec numeral_Bit0_div_2 mod_2_eq_odd)
 
 lemma bit_of_nat_iff_bit [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
@@ -2600,7 +2611,7 @@
 lemma [code]:
   \<open>unset_bit 0 m = 2 * (m div 2)\<close>
   \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m n :: nat
-  by (simp_all add: unset_bit_Suc)
+  by (simp_all add: unset_bit_0 unset_bit_Suc)
 
 lemma push_bit_of_Suc_0 [simp]:
   \<open>push_bit n (Suc 0) = 2 ^ n\<close>
@@ -2778,7 +2789,7 @@
 
 lemma bit_numeral_Bit1_Suc_iff [simp]:
   \<open>bit (numeral (Num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
-  by (simp add: bit_Suc numeral_Bit1_div_2)
+  by (simp add: bit_Suc numeral_Bit0_div_2)
 
 lemma bit_numeral_rec:
   \<open>bit (numeral (Num.Bit0 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc m \<Rightarrow> bit (numeral w) m)\<close>
@@ -3278,6 +3289,86 @@
 
 end
 
+context semiring_bit_operations
+begin
+
+lemma push_bit_eq_pow:
+  \<open>push_bit (numeral n) 1 = numeral (Num.pow (Num.Bit0 Num.One) n)\<close>
+  by simp
+
+lemma set_bit_of_0 [simp]:
+  \<open>set_bit n 0 = 2 ^ n\<close>
+  by (simp add: set_bit_eq_or)
+
+lemma unset_bit_of_0 [simp]:
+  \<open>unset_bit n 0 = 0\<close>
+  by (simp add: unset_bit_eq_or_xor)
+
+lemma flip_bit_of_0 [simp]:
+  \<open>flip_bit n 0 = 2 ^ n\<close>
+  by (simp add: flip_bit_eq_xor)
+
+lemma set_bit_0_numeral_eq [simp]:
+  \<open>set_bit 0 (numeral Num.One) = 1\<close>
+  \<open>set_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+  \<open>set_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit1 m)\<close>
+  by (simp_all add: set_bit_0)
+
+lemma set_bit_numeral_eq_or [simp]:
+  \<open>set_bit (numeral n) (numeral m) = numeral m OR push_bit (numeral n) 1\<close>
+  by (fact set_bit_eq_or)
+
+lemma unset_bit_0_numeral_eq_and_not' [simp]:
+  \<open>unset_bit 0 (numeral Num.One) = 0\<close>
+  \<open>unset_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit0 m)\<close>
+  \<open>unset_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+  by (simp_all add: unset_bit_0)
+
+lemma unset_bit_numeral_eq_or [simp]:
+  \<open>unset_bit (numeral n) (numeral m) =
+    (case and_not_num m (Num.pow (Num.Bit0 Num.One) n)
+     of None \<Rightarrow> 0
+      | Some q \<Rightarrow> numeral q)\<close> (is \<open>?lhs = _\<close>)
+proof -
+  have \<open>?lhs = of_nat (unset_bit (numeral n) (numeral m))\<close>
+    by (simp add: of_nat_unset_bit_eq)
+  also have \<open>unset_bit (numeral n) (numeral m) = nat (unset_bit (numeral n) (numeral m))\<close>
+    by (simp flip: int_int_eq add: Bit_Operations.of_nat_unset_bit_eq)
+  finally have *: \<open>?lhs = of_nat (nat (unset_bit (numeral n) (numeral m)))\<close> .
+  show ?thesis
+    by (simp only: * unset_bit_eq_and_not Bit_Operations.push_bit_eq_pow int_numeral_and_not_num)
+      (auto split: option.splits)
+qed
+
+lemma flip_bit_0_numeral_eq_or [simp]:
+  \<open>flip_bit 0 (numeral Num.One) = 0\<close>
+  \<open>flip_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+  \<open>flip_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+  by (simp_all add: flip_bit_0)
+
+lemma flip_bit_numeral_eq_xor [simp]:
+  \<open>flip_bit (numeral n) (numeral m) = numeral m XOR push_bit (numeral n) 1\<close>
+  by (fact flip_bit_eq_xor)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma set_bit_minus_numeral_eq_or [simp]:
+  \<open>set_bit (numeral n) (- numeral m) = - numeral m OR push_bit (numeral n) 1\<close>
+  by (fact set_bit_eq_or)
+
+lemma unset_bit_minus_numeral_eq_and_not [simp]:
+  \<open>unset_bit (numeral n) (- numeral m) = - numeral m AND NOT (push_bit (numeral n) 1)\<close>
+  by (fact unset_bit_eq_and_not)
+
+lemma flip_bit_minus_numeral_eq_xor [simp]:
+  \<open>flip_bit (numeral n) (- numeral m) = - numeral m XOR push_bit (numeral n) 1\<close>
+  by (fact flip_bit_eq_xor)
+
+end
+
 lemma xor_int_code [code]:
   fixes i j :: int shows
   \<open>0 XOR j = j\<close>
diff -r 88060e644af7 -r 9a85d296ab81 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 21 11:15:34 2025 +0100
+++ b/src/HOL/List.thy	Tue Jan 21 11:17:05 2025 +0100
@@ -263,6 +263,15 @@
 replicate_0: "replicate 0 x = []" |
 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 
+overloading pow_list == "compow :: nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+begin
+
+primrec pow_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pow_list 0 xs = []" |
+"pow_list (Suc n) xs = xs @ pow_list n xs"
+
+end
+
 text \<open>
   Function \<open>size\<close> is overloaded for all datatypes. Users may
   refer to the list version as \<open>length\<close>.\<close>
@@ -1168,7 +1177,7 @@
 by(blast dest:map_injective)
 
 lemma inj_mapI: "inj f \<Longrightarrow> inj (map f)"
-by (iprover dest: map_injective injD intro: inj_onI)
+by (rule list.inj_map)
 
 lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
   by (metis (no_types, opaque_lifting) injI list.inject list.simps(9) the_inv_f_f)
@@ -1180,7 +1189,7 @@
   by (blast intro:inj_onI dest:inj_onD map_inj_on)
 
 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
-by (induct xs, auto)
+by (rule list.map_ident_strong)
 
 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
 by (induct xs) auto
@@ -1218,6 +1227,9 @@
 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
 by (induct xs) auto
 
+lemma rev_involution[simp]: "rev \<circ> rev = id"
+by auto
+
 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
 by auto
 
@@ -1284,6 +1296,21 @@
   qed
 qed simp
 
+lemma rev_induct2:
+  "\<lbrakk> P [] [];
+  \<And>x xs. P (xs @ [x]) [];
+  \<And>y ys. P [] (ys @ [y]);
+  \<And>x xs y ys. P xs ys  \<Longrightarrow> P (xs @ [x]) (ys @ [y]) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+proof (induct xs arbitrary: ys rule: rev_induct)
+  case Nil
+  then show ?case using rev_induct[of "P []"] by presburger
+next
+  case (snoc x xs)
+  hence "P xs ys'" for ys' by simp
+  then show ?case by (simp add: rev_induct snoc.prems(2,4))
+qed
+
 lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)"
 by (induct xs rule: rev_induct) auto
 
@@ -4404,6 +4431,10 @@
   "\<lbrakk> inj_on f (set xs); x \<in> set xs \<rbrakk> \<Longrightarrow> count_list (map f xs) (f x) = count_list xs x"
 by (induction xs) (simp, fastforce)
 
+lemma count_list_map_conv:
+assumes "inj f" shows "count_list (map f xs) (f x) = count_list xs x"
+by (induction xs) (simp_all add: inj_eq[OF assms])
+
 lemma count_list_rev[simp]: "count_list (rev xs) x = count_list xs x"
 by (induction xs) auto
 
@@ -4714,6 +4745,9 @@
   "concat (replicate i []) = []"
   by (induct i) (auto simp add: map_replicate_const)
 
+lemma concat_replicate_single[simp]: "concat (replicate m [a]) = replicate m a"
+by(induction m) auto
+
 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
 by (induct n) auto
 
@@ -4812,6 +4846,134 @@
 by (subst foldr_fold [symmetric]) simp_all
 
 
+subsubsection \<open>\<^term>\<open>xs ^^ n\<close>\<close>
+
+context
+begin
+
+interpretation monoid_mult "[]" "append"
+  rewrites "power u n = u ^^ n"
+proof-
+  show "class.monoid_mult [] (@)"
+    by (unfold_locales, simp_all)
+  show "power.power [] (@) u n = u ^^ n"
+    by(induction n) (auto simp add: power.power.simps)
+qed
+
+\<comment> \<open>inherited power properties\<close>
+
+lemmas pow_list_zero = power.power_0 and
+  pow_list_one = power_Suc0_right and
+  pow_list_1 = power_one_right and
+  pow_list_Nil = power_one and
+  pow_list_2 = power2_eq_square and
+  pow_list_Suc = power_Suc and
+  pow_list_Suc2 = power_Suc2 and
+  pow_list_comm = power_commutes and
+  pow_list_add = power_add and
+  pow_list_eq_if = power_eq_if and
+  pow_list_mult = power_mult and
+  pow_list_commuting_commutes = power_commuting_commutes
+
+end
+
+lemma pow_list_alt: "xs^^n = concat (replicate n xs)"
+by (induct n) auto
+
+lemma pow_list_single: "[a] ^^ m = replicate m a"
+by(simp add: pow_list_alt)
+
+lemma length_pow_list_single [simp]: "length([a] ^^ n) = n"
+by (simp add: pow_list_single)
+
+lemma nth_pow_list_single: "i < m \<Longrightarrow> ([a] ^^ m) ! i = a"
+by (simp add: pow_list_single)
+
+lemma pow_list_not_NilD: "xs ^^ m \<noteq> [] \<Longrightarrow> 0 < m"
+by (cases m) auto
+
+lemma length_pow_list:  "length(xs ^^ k) = k * length xs"
+by (induction k) simp+
+
+lemma pow_list_set: "set (w ^^ Suc k) = set w"
+by (induction k)(simp_all)
+
+lemma pow_list_slide: "xs @ (ys @ xs) ^^ n  @ ys = (xs @ ys)^^(Suc n)"
+by (induction n) simp+
+
+lemma hd_pow_list: "0 < n \<Longrightarrow> hd(xs ^^ n) = hd xs"
+by(auto simp: pow_list_alt hd_append gr0_conv_Suc)
+
+lemma rev_pow_list: "rev (xs ^^ m) = (rev xs) ^^ m"
+by (induction m)(auto simp: pow_list_comm)
+
+lemma eq_pow_list_iff_eq_exp[simp]: assumes "xs \<noteq> []" shows "xs ^^ k = xs ^^ m \<longleftrightarrow> k = m"
+proof
+  assume "k = m" thus "xs ^^ k = xs ^^ m" by simp
+next
+  assume "xs ^^ k = xs ^^ m"
+  thus "k = m" using \<open>xs \<noteq> []\<close>[folded length_0_conv]
+    by (metis length_pow_list mult_cancel2)
+qed
+
+lemma pow_list_Nil_iff_0: "xs \<noteq> [] \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow> m = 0"
+by (simp add: pow_list_eq_if)
+
+lemma pow_list_Nil_iff_Nil: "0 < m \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow>  xs = []"
+by (cases xs) (auto simp add: pow_list_Nil pow_list_Nil_iff_0)
+
+lemma pow_eq_eq:
+  assumes "xs ^^ k = ys ^^ k" and "0 < k"
+  shows "(xs::'a list) = ys"
+proof-
+  have "length xs = length ys"
+    using assms(1) length_pow_list by (metis nat_mult_eq_cancel1[OF \<open>0 < k\<close>])
+  thus ?thesis by (metis Suc_pred append_eq_append_conv assms(1,2) pow_list.simps(2))
+qed
+
+lemma map_pow_list[simp]: "map f (xs ^^ k) = (map f xs) ^^ k"
+by (induction k) simp_all
+
+lemma concat_pow_list: "concat (xs ^^ k) = (concat xs) ^^ k"
+by (induction k) simp_all
+
+lemma concat_pow_list_single[simp]: "concat ([a] ^^ k) = a ^^ k"
+by (simp add: pow_list_alt)
+
+lemma pow_list_single_Nil_iff: "[a] ^^ n = [] \<longleftrightarrow> n = 0"
+by (simp add: pow_list_single)
+
+lemma hd_pow_list_single: "k \<noteq> 0 \<Longrightarrow> hd ([a] ^^ k) = a"
+by (cases k) simp+
+
+lemma index_pow_mod: "i < length(xs ^^ k) \<Longrightarrow> (xs ^^ k)!i = xs!(i mod length xs)"
+proof(induction k)
+  have aux:  "length(xs ^^ Suc l) = length(xs ^^ l) + length xs" for l
+    by simp
+  have aux1: "length (xs ^^ l) \<le> i \<Longrightarrow> i < length(xs ^^ l) + length xs \<Longrightarrow>  i mod length xs = i -  length(xs^^l)" for l
+    unfolding length_pow_list[of l xs]
+     using less_diff_conv2[of "l * length xs" i "length xs", unfolded add.commute[of "length xs"  "l * length xs"]]
+       le_add_diff_inverse[of "l*length xs" i]
+    by (simp add: mod_nat_eqI)
+  case (Suc k)
+  show ?case
+    unfolding aux sym[OF pow_list_Suc2[symmetric]] nth_append le_mod_geq
+    using aux1[ OF _ Suc.prems[unfolded aux]]
+      Suc.IH pow_list_Suc2[symmetric] Suc.prems[unfolded aux] leI[of i "length(xs ^^ k)"] by presburger
+qed auto
+
+lemma unique_letter_word: assumes "\<And>c. c \<in> set w \<Longrightarrow> c = a" shows "w = [a] ^^ length w"
+  using assms proof (induction w)
+  case (Cons b w)
+  have "[a] ^^ length w = w" using Cons.IH[OF Cons.prems[OF list.set_intros(2)]]..
+  then show "b # w = [a] ^^ length(b # w)"
+    unfolding Cons.prems[OF list.set_intros(1)] by auto
+qed simp
+
+lemma count_list_pow_list: "count_list (w ^^ k) a = k * (count_list w a)"
+by (induction k) simp+
+
+
 subsubsection \<open>\<^const>\<open>enumerate\<close>\<close>
 
 lemma enumerate_simps [simp, code]:
@@ -6612,8 +6774,7 @@
 lemma Cons_in_lists_iff[simp]: "x#xs \<in> lists A \<longleftrightarrow> x \<in> A \<and> xs \<in> lists A"
 by auto
 
-lemma append_in_listsp_conv [iff]:
-     "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
+lemma append_in_listsp_conv [iff]: "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
 by (induct xs) auto
 
 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
@@ -6634,6 +6795,9 @@
 
 lemmas in_listsI [intro!] = in_listspI [to_set]
 
+lemma mono_lists: "mono lists"
+unfolding mono_def by auto
+
 lemma lists_eq_set: "lists A = {xs. set xs \<le> A}"
 by auto
 
@@ -6650,6 +6814,41 @@
   then show ?thesis by auto
 qed
 
+lemma inj_on_map_lists: assumes "inj_on f A"
+  shows "inj_on (map f) (lists A)"
+proof
+  fix xs ys
+  assume "xs \<in> lists A" and "ys \<in> lists A" and "map f xs = map f ys"
+  have "x = y" if "x \<in> set xs" and "y \<in> set ys" and  "f x =  f y"  for x y
+    using in_listsD[OF \<open>xs \<in> lists A\<close>, rule_format, OF \<open>x \<in> set xs\<close>]
+          in_listsD[OF \<open>ys \<in> lists A\<close>, rule_format, OF \<open>y \<in> set ys\<close>]
+         \<open>inj_on f A\<close>[unfolded inj_on_def, rule_format, OF _ _ \<open>f x =  f y\<close>] by blast
+  from list.inj_map_strong[OF this  \<open>map f xs = map f ys\<close>]
+  show "xs = ys".
+qed
+
+lemma bij_lists: "bij_betw f X Y \<Longrightarrow> bij_betw (map f) (lists X) (lists Y)"
+unfolding bij_betw_def using inj_on_map_lists lists_image by metis
+
+lemma replicate_in_lists: "a \<in> A \<Longrightarrow> replicate k a \<in> lists A"
+by (induction k) auto
+
+lemma sing_pow_lists: "a \<in> A \<Longrightarrow> [a] ^^ n \<in> lists A"
+by (induction n) auto
+
+lemma one_generated_list_power: "u \<in> lists {x} \<Longrightarrow> \<exists>k. concat u = x ^^ k"
+proof(induction u rule: lists.induct)
+  case Nil
+  then show ?case by (metis concat.simps(1) pow_list.simps(1))
+next
+  case Cons
+  then show ?case by (metis concat.simps(2) pow_list_Suc singletonD)
+qed
+
+lemma pow_list_in_lists: "0 < k \<Longrightarrow> u ^^ k \<in> lists B \<Longrightarrow> u \<in> lists B"
+by (metis Suc_pred in_lists_conv_set pow_list_set)
+
+
 subsubsection \<open>Inductive definition for membership\<close>
 
 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
diff -r 88060e644af7 -r 9a85d296ab81 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jan 21 11:15:34 2025 +0100
+++ b/src/HOL/ROOT	Tue Jan 21 11:17:05 2025 +0100
@@ -694,6 +694,7 @@
     BigO
     BinEx
     Birthday_Paradox
+    Bit_Operation_Calculations
     Bubblesort
     CTL
     Cartouche_Examples
diff -r 88060e644af7 -r 9a85d296ab81 src/HOL/ex/Bit_Operation_Calculations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Bit_Operation_Calculations.thy	Tue Jan 21 11:17:05 2025 +0100
@@ -0,0 +1,145 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Tests for simplifying bit operations on ground terms\<close>
+
+theory Bit_Operation_Calculations
+  imports
+    "HOL.Bit_Operations"
+    "HOL-Library.Word"
+begin
+
+unbundle bit_operations_syntax
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale unsigned_computations =
+  fixes type :: \<open>'a::semiring_bit_operations itself\<close>
+begin
+
+definition computations where
+  \<open>computations = (
+    [bit (473514 :: 'a) 5],
+    [473514 AND 767063 :: 'a],
+    [473514 OR 767063 :: 'a],
+    [473514 XOR 767063 :: 'a],
+    mask 11 :: 'a,
+    [set_bit 15 473514 :: 'a],
+    [unset_bit 13 473514 :: 'a],
+    [flip_bit 15 473514 :: 'a],
+    [push_bit 12 473514 :: 'a],
+    [drop_bit 12 65344 :: 'a],
+    [take_bit 12 473514 :: 'a]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True],
+    [208898 :: 'a::semiring_bit_operations],
+    [1031679 :: 'a],
+    [822781 :: 'a],
+    2047 :: 'a,
+    [506282 :: 'a],
+    [465322 :: 'a],
+    [506282 :: 'a],
+    [1939513344 :: 'a],
+    [15 :: 'a],
+    [2474 :: 'a]
+  )\<close>
+
+lemmas evaluation_simps = computations_def results_def mask_numeral
+   \<comment> \<open>Expressions like \<term>\<open>mask 42\<close> are deliberately not simplified by default\<close>
+
+end
+
+global_interpretation unsigned_computations_nat: unsigned_computations \<open>TYPE(nat)\<close>
+  defines unsigned_computations_nat = unsigned_computations_nat.computations
+    and unsigned_results_nat = unsigned_computations_nat.results .
+
+lemma \<open>unsigned_computations_nat.computations = unsigned_computations_nat.results\<close>
+  by (simp add: unsigned_computations_nat.evaluation_simps)
+
+global_interpretation unsigned_computations_int: unsigned_computations \<open>TYPE(int)\<close>
+  defines unsigned_computations_int = unsigned_computations_int.computations
+    and unsigned_results_int = unsigned_computations_int.results .
+
+lemma \<open>unsigned_computations_int.computations = unsigned_computations_int.results\<close>
+  by (simp add: unsigned_computations_int.evaluation_simps)
+
+global_interpretation unsigned_computations_word16: unsigned_computations \<open>TYPE(16 word)\<close>
+  defines unsigned_computations_word16 = unsigned_computations_word16.computations
+    and unsigned_results_word16 = unsigned_computations_word16.results .
+
+lemma \<open>unsigned_computations_word16 = unsigned_results_word16\<close>
+  by (simp add: unsigned_computations_word16.evaluation_simps)
+
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale signed_computations =
+  fixes type :: \<open>'a::ring_bit_operations itself\<close>
+begin
+
+definition computations where
+  \<open>computations = (
+    [bit (- 805167 :: 'a) 7],
+    [- 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: 'a],
+    [- 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: 'a],
+    [- 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: 'a],
+    [NOT 473513, NOT (- 805167) :: 'a],
+    [set_bit 11 (- 805167) :: 'a],
+    [unset_bit 12 (- 805167) :: 'a],
+    [flip_bit 12 (- 805167) :: 'a],
+    [push_bit 12 (- 805167) :: 'a],
+    [take_bit 12 (- 805167) :: 'a],
+    [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: 'a]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True],
+    [242769, 209184, - 839103 :: 'a],
+    [- 280873, - 50197, - 280591 :: 'a],
+    [- 523642, - 259381, 558512 :: 'a],
+    [- 473514, 805166 :: 'a],
+    [- 803119 :: 'a],
+    [- 809263 :: 'a],
+    [- 809263 :: 'a],
+    [- 3297964032 :: 'a],
+    [1745 :: 'a],
+    [- 1622, - 2351 :: 'a]
+  )\<close>
+
+lemmas evaluation_simps = computations_def results_def
+
+end
+
+global_interpretation signed_computations_int: signed_computations \<open>TYPE(int)\<close>
+  defines signed_computations_int = signed_computations_int.computations
+    and signed_results_int = signed_computations_int.results .
+
+lemma \<open>signed_computations_int.computations = signed_computations_int.results\<close>
+  by (simp add: signed_computations_int.evaluation_simps)
+
+global_interpretation signed_computations_word16: signed_computations \<open>TYPE(16 word)\<close>
+  defines signed_computations_word16 = signed_computations_word16.computations
+    and signed_results_word16 = signed_computations_word16.results .
+
+lemma \<open>signed_computations_word16 = signed_results_word16\<close>
+  by (simp add: signed_computations_word16.evaluation_simps)
+
+
+subsection \<open>Special cases on particular type instances\<close>
+
+lemma
+  \<open>drop_bit 12 (- 17405 :: int) = - 5\<close>
+  by simp
+
+lemma
+  \<open>signed_drop_bit 12 (- 17405 :: 16 word) = - 5\<close>
+  by simp
+
+lemma
+  \<open>drop_bit 12 (- 17405 :: 16 word) = 11\<close>
+  by simp
+
+end
diff -r 88060e644af7 -r 9a85d296ab81 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Jan 21 11:15:34 2025 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Jan 21 11:17:05 2025 +0100
@@ -384,16 +384,27 @@
     val serializer = (#serializer o #language) target;
   in { serializer = serializer, data = data, modify = modify } end;
 
-fun project_program_for_syms ctxt syms_hidden syms1 program1 =
+fun report_unimplemented ctxt program requested unimplemented =
   let
-    val syms2 = subtract (op =) syms_hidden syms1;
+    val deps = flat (map_product (fn req => fn unimpl =>
+      Code_Symbol.Graph.irreducible_paths program (req, Constant unimpl)) requested unimplemented)
+    val pretty_dep = space_implode " -> " o map (Code_Symbol.quote ctxt)
+  in
+    error ("No code equations for "
+      ^ commas (map (Proof_Context.markup_const ctxt) unimplemented)
+      ^ ",\nrequested by dependencies\n"
+      ^ space_implode "\n" (map pretty_dep deps))
+  end;
+
+fun project_program_for_syms ctxt syms_hidden requested1 program1 =
+  let
+    val requested2 = subtract (op =) syms_hidden requested1;
     val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
     val unimplemented = Code_Thingol.unimplemented program2;
     val _ =
       if null unimplemented then ()
-      else error ("No code equations for " ^
-        commas (map (Proof_Context.markup_const ctxt) unimplemented));
-    val syms3 = Code_Symbol.Graph.all_succs program2 syms2;
+      else report_unimplemented ctxt program2 requested2 unimplemented;
+    val syms3 = Code_Symbol.Graph.all_succs program2 requested2;
     val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
   in program3 end;