# HG changeset patch
# User haftmann
# Date 1705175412 0
# Node ID c7cb1bf6efa0f308f3c99e47df3a6eb51c862219
# Parent  590a01e3efb49a259520224c11b03a603f2eaecf
consolidated name of lemma analogously to nat/int/word_bit_induct

diff -r 590a01e3efb4 -r c7cb1bf6efa0 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Fri Jan 12 17:00:35 2024 +0100
+++ b/src/HOL/Bit_Operations.thy	Sat Jan 13 19:50:12 2024 +0000
@@ -10,7 +10,7 @@
 subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
-  assumes bits_induct [case_names stable rec]:
+  assumes bit_induct [case_names stable rec]:
     \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
      \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
         \<Longrightarrow> P a\<close>
@@ -123,7 +123,7 @@
 
 lemma bit_iff_idd_imp_stable:
   \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
-using that proof (induction a rule: bits_induct)
+using that proof (induction a rule: bit_induct)
   case (stable a)
   then show ?case
     by simp
@@ -192,7 +192,7 @@
     then show ?thesis
       by (rule that[unfolded possible_bit_def])
   qed
-  then show ?thesis proof (induction a arbitrary: b rule: bits_induct)
+  then show ?thesis proof (induction a arbitrary: b rule: bit_induct)
     case (stable a)
     from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
       by (simp add: bit_0)
@@ -3719,7 +3719,7 @@
 
       \<^item> Equality rule: @{thm bit_eqI [where ?'a = int, no_vars]}
 
-      \<^item> Induction rule: @{thm bits_induct [where ?'a = int, no_vars]}
+      \<^item> Induction rule: @{thm bit_induct [where ?'a = int, no_vars]}
 
   \<^item> Typical operations are characterized as follows:
 
diff -r 590a01e3efb4 -r c7cb1bf6efa0 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jan 12 17:00:35 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Jan 13 19:50:12 2024 +0000
@@ -348,7 +348,7 @@
   is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
+  (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff
@@ -1107,7 +1107,7 @@
   is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
+  (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff and_rec or_rec xor_rec