src/HOL/Parity.thy

     and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
     and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
     and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
     and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
     and even_mult_exp_div_exp_iff: \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> m > n \<or> 2 ^ n = 0 \<or> (m \<le> n \<and> even (a div 2 ^ (n - m)))\<close>
+  fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
+  assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
 begin
+
+text \<open>
+  Having \<^const>\<open>bit\<close> as definitional class operation
+  takes into account that specific instances can be implemented
+  differently wrt. code generation.
+\<close>
 
 lemma bits_div_by_0 [simp]:
   \<open>a div 0 = 0\<close>
   by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
 

 
 lemma bits_one_mod_two_eq_one [simp]:
   \<open>1 mod 2 = 1\<close>
   by (simp add: mod2_eq_if)
 
-definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
-  where \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
-
 lemma bit_0 [simp]:
   \<open>bit a 0 \<longleftrightarrow> odd a\<close>
-  by (simp add: bit_def)
+  by (simp add: bit_iff_odd)
 
 lemma bit_Suc:
   \<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
-  using div_exp_eq [of a 1 n] by (simp add: bit_def)
+  using div_exp_eq [of a 1 n] by (simp add: bit_iff_odd)
 
 lemma bit_rec:
   \<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
   by (cases n) (simp_all add: bit_Suc)
 
 lemma bit_0_eq [simp]:
   \<open>bit 0 = bot\<close>
-  by (simp add: fun_eq_iff bit_def)
+  by (simp add: fun_eq_iff bit_iff_odd)
 
 context
   fixes a
   assumes stable: \<open>a div 2 = a\<close>
 begin

     using \<open>a div 2 = a\<close> by (simp add: hyp)
 qed
 
 lemma exp_eq_0_imp_not_bit:
   \<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
-  using that by (simp add: bit_def)
+  using that by (simp add: bit_iff_odd)
 
 lemma bit_eqI:
   \<open>a = b\<close> if \<open>\<And>n. 2 ^ n \<noteq> 0 \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
 proof -
   have \<open>bit a n \<longleftrightarrow> bit b n\<close> for n

   \<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
   by (auto intro: bit_eqI)
 
 lemma bit_exp_iff:
   \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
-  by (auto simp add: bit_def exp_div_exp_eq)
+  by (auto simp add: bit_iff_odd exp_div_exp_eq)
 
 lemma bit_1_iff:
   \<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
   using bit_exp_iff [of 0 n] by simp
 

   \<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
   using bit_exp_iff [of 1 n] by auto
 
 lemma even_bit_succ_iff:
   \<open>bit (1 + a) n \<longleftrightarrow> bit a n \<or> n = 0\<close> if \<open>even a\<close>
-  using that by (cases \<open>n = 0\<close>) (simp_all add: bit_def)
+  using that by (cases \<open>n = 0\<close>) (simp_all add: bit_iff_odd)
 
 lemma odd_bit_iff_bit_pred:
   \<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close>
 proof -
   from \<open>odd a\<close> obtain b where \<open>a = 2 * b + 1\<close> ..

 qed
 
 lemma bit_double_iff:
   \<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close>
   using even_mult_exp_div_exp_iff [of a 1 n]
-  by (cases n, auto simp add: bit_def ac_simps)
+  by (cases n, auto simp add: bit_iff_odd ac_simps)
 
 lemma bit_eq_rec:
   \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
 proof
   assume ?P

   qed
 qed
 
 lemma bit_mod_2_iff [simp]:
   \<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
-  by (cases a rule: parity_cases) (simp_all add: bit_def)
+  by (cases a rule: parity_cases) (simp_all add: bit_iff_odd)
 
 lemma bit_mask_iff:
   \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
-  by (simp add: bit_def even_mask_div_iff not_le)
+  by (simp add: bit_iff_odd even_mask_div_iff not_le)
 
 lemma bit_Numeral1_iff [simp]:
   \<open>bit (numeral Num.One) n \<longleftrightarrow> n = 0\<close>
   by (simp add: bit_rec)
 

         by simp
     qed
   qed
 qed
 
-instance nat :: semiring_bits
+instantiation nat :: semiring_bits
+begin
+
+definition bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where \<open>bit_nat m n \<longleftrightarrow> odd (m div 2 ^ n)\<close>
+
+instance
 proof
   show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
     and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
     for P and n :: nat
   proof (induction n rule: nat_bit_induct)

   show \<open>even (q * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::nat) ^ n = 0 \<or> m \<le> n \<and> even (q div 2 ^ (n - m))\<close>
     for m n q r :: nat
     apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
     apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc)
     done
-qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff bit_nat_def)
+
+end
 
 lemma int_bit_induct [case_names zero minus even odd]:
   "P k" if zero_int: "P 0"
     and minus_int: "P (- 1)"
     and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"

     finally show ?case
       using odd by simp
   qed
 qed
 
-instance int :: semiring_bits
+instantiation int :: semiring_bits
+begin
+
+definition bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where \<open>bit_int k n \<longleftrightarrow> odd (k div 2 ^ n)\<close>
+
+instance
 proof
   show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
     and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
     for P and k :: int
   proof (induction k rule: int_bit_induct)

   show \<open>even (k * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::int) ^ n = 0 \<or> m \<le> n \<and> even (k div 2 ^ (n - m))\<close>
     for m n :: nat and k l :: int
     apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
     apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2))
     done
-qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le bit_int_def)
+
+end
 
 class semiring_bit_shifts = semiring_bits +
   fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
   fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
+  fixes take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  assumes take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
 begin
-
-definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
 
 text \<open>
   Logically, \<^const>\<open>push_bit\<close>,
   \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
   as separate operations makes proofs easier, otherwise proof automation
   would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
   algebraic relationships between those operations.
   Having
-  \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations
+  them as definitional class operations
   takes into account that specific instances of these can be implemented
   differently wrt. code generation.
 \<close>
 
 lemma bit_iff_odd_drop_bit:
   \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
-  by (simp add: bit_def drop_bit_eq_div)
+  by (simp add: bit_iff_odd drop_bit_eq_div)
 
 lemma even_drop_bit_iff_not_bit:
   \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
   by (simp add: bit_iff_odd_drop_bit)
 

   \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
   by (simp add: push_bit_eq_mult) auto
 
 lemma bit_push_bit_iff:
   \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> (n < m \<or> bit a (n - m))\<close>
-  by (auto simp add: bit_def push_bit_eq_mult even_mult_exp_div_exp_iff)
+  by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
 
 lemma bit_drop_bit_eq:
   \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
-  by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div)
+  by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
 
 lemma bit_take_bit_iff:
   \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
-  by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div)
+  by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)
 
 lemma stable_imp_drop_bit_eq:
   \<open>drop_bit n a = a\<close>
   if \<open>a div 2 = a\<close>
   by (induction n) (simp_all add: that drop_bit_Suc)

   where \<open>push_bit_nat n m = m * 2 ^ n\<close>
 
 definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
   where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
 
-instance proof
-  show \<open>push_bit n m = m * 2 ^ n\<close> for n m :: nat
-    by (simp add: push_bit_nat_def)
-  show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
-    by (simp add: drop_bit_nat_def)
-qed
+definition take_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>take_bit_nat n m = m mod 2 ^ n\<close>
+
+instance
+  by standard (simp_all add: push_bit_nat_def drop_bit_nat_def take_bit_nat_def)
 
 end
 
 instantiation int :: semiring_bit_shifts
 begin

   where \<open>push_bit_int n k = k * 2 ^ n\<close>
 
 definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>drop_bit_int n k = k div 2 ^ n\<close>
 
-instance proof
-  show \<open>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
-    by (simp add: push_bit_int_def)
-  show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
-    by (simp add: drop_bit_int_def)
-qed
+definition take_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>take_bit_int n k = k mod 2 ^ n\<close>
+
+instance
+  by standard (simp_all add: push_bit_int_def drop_bit_int_def take_bit_int_def)
 
 end
 
 lemma bit_push_bit_iff_nat:
   \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat

   have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
     by simp
   also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
     by (simp add: of_nat_div)
   finally show ?thesis
-    by (simp add: bit_def semiring_bits_class.bit_def)
+    by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
 qed
 
 lemma of_nat_push_bit:
   \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
   by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)