bit accessor and fundamental properties

--- a/src/HOL/Parity.thy	Fri Nov 29 21:53:02 2019 +0100
+++ b/src/HOL/Parity.thy	Wed Nov 27 16:54:33 2019 +0000
@@ -30,6 +30,10 @@
   using assms by (cases "even a")
     (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric])
 
+lemma odd_of_bool_self [simp]:
+  \<open>odd (of_bool p) \<longleftrightarrow> p\<close>
+  by (cases p) simp_all
+
 lemma not_mod_2_eq_0_eq_1 [simp]:
   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   by (cases a rule: parity_cases) simp_all
@@ -562,11 +566,10 @@
 qed
 
 
-subsection \<open>Abstract bit shifts\<close>
+subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
-  assumes bit_eq_rec: \<open>a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
-    and bit_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>
@@ -629,6 +632,124 @@
   \<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)
+
+lemma bit_Suc [simp]:
+  \<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)
+
+context
+  fixes a
+  assumes stable: \<open>a div 2 = a\<close>
+begin
+
+lemma stable_imp_add_self:
+  \<open>a + a mod 2 = 0\<close>
+proof -
+  have \<open>a div 2 * 2 + a mod 2 = a\<close>
+    by (fact div_mult_mod_eq)
+  then have \<open>a * 2 + a mod 2 = a\<close>
+    by (simp add: stable)
+  then show ?thesis
+    by (simp add: mult_2_right ac_simps)
+qed
+
+lemma stable_imp_bit_iff_odd:
+  \<open>bit a n \<longleftrightarrow> odd a\<close>
+  by (induction n) (simp_all add: stable)
+
+end
+
+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: bit_induct)
+  case (stable a)
+  then show ?case
+    by simp
+next
+  case (rec a b)
+  from rec.prems [of 1] have [simp]: \<open>b = odd a\<close>
+    by (simp add: rec.hyps)
+  from rec.hyps have hyp: \<open>(of_bool (odd a) + 2 * a) div 2 = a\<close>
+    by simp
+  have \<open>bit a n \<longleftrightarrow> odd a\<close> for n
+    using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp)
+  then have \<open>a div 2 = a\<close>
+    by (rule rec.IH)
+  then have \<open>of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\<close>
+    by (simp add: ac_simps)
+  also have \<open>\<dots> = a\<close>
+    using mult_div_mod_eq [of 2 a]
+    by (simp add: of_bool_odd_eq_mod_2)
+  finally show ?case
+    using \<open>a div 2 = a\<close> by (simp add: hyp)
+qed
+
+lemma bit_eqI:
+  \<open>a = b\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> bit b n\<close>
+using that 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
+  have \<open>b div 2 = b\<close>
+  proof (rule bit_iff_idd_imp_stable)
+    fix n
+    from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close>
+      by simp
+    also have \<open>bit a n \<longleftrightarrow> odd a\<close>
+      using stable by (simp add: stable_imp_bit_iff_odd)
+    finally show \<open>bit b n \<longleftrightarrow> odd b\<close>
+      by (simp add: **)
+  qed
+  from ** have \<open>a mod 2 = b mod 2\<close>
+    by (simp add: mod2_eq_if)
+  then have \<open>a mod 2 + (a + b) = b mod 2 + (a + b)\<close>
+    by simp
+  then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
+    by (simp add: ac_simps)
+  with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
+    by (simp add: stable_imp_add_self)
+next
+  case (rec a p)
+  from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
+    by simp
+  from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
+    using rec.prems [of \<open>Suc n\<close>] by simp
+  then have \<open>a = b div 2\<close>
+    by (rule rec.IH)
+  then have \<open>2 * a = 2 * (b div 2)\<close>
+    by simp
+  then have \<open>b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\<close>
+    by simp
+  also have \<open>\<dots> = b\<close>
+    by (fact mod_mult_div_eq)
+  finally show ?case
+    by (auto simp add: mod2_eq_if)
+qed
+
+lemma bit_eq_iff:
+  \<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
+  by (auto intro: bit_eqI)
+
+lemma bit_eq_rec:
+  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
+  apply (simp add: bit_eq_iff)
+  apply auto
+  using bit_0 apply blast
+  using bit_0 apply blast
+  using bit_Suc apply blast
+  using bit_Suc apply blast
+     apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq)
+    apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq)
+   apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq)
+  apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq)
+  done
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
@@ -662,9 +783,6 @@
 
 instance nat :: semiring_bits
 proof
-  show \<open>m = n \<longleftrightarrow> (even m \<longleftrightarrow> even n) \<and> m div 2 = n div 2\<close>
-    for m n :: nat
-    by (auto dest: odd_two_times_div_two_succ)
   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
@@ -753,9 +871,6 @@
 
 instance int :: semiring_bits
 proof
-  show \<open>k = l \<longleftrightarrow> (even k \<longleftrightarrow> even l) \<and> k div 2 = l div 2\<close>
-    for k l :: int
-    by (auto dest: odd_two_times_div_two_succ)
   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
@@ -954,6 +1069,14 @@
     by simp
 qed
 
+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)
+
+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)
+
 end
 
 instantiation nat :: semiring_bit_shifts

--- a/src/HOL/Word/Bits_Int.thy	Fri Nov 29 21:53:02 2019 +0100
+++ b/src/HOL/Word/Bits_Int.thy	Wed Nov 27 16:54:33 2019 +0000
@@ -1623,7 +1623,8 @@
   apply (case_tac bit, auto)
   done
 
-lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
+lemma mod_BIT:
+  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" for bit
 proof -
   have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
     by (simp add: mod_mult_mult1)

--- a/src/HOL/ex/Bit_Operations.thy	Fri Nov 29 21:53:02 2019 +0100
+++ b/src/HOL/ex/Bit_Operations.thy	Wed Nov 27 16:54:33 2019 +0000
@@ -26,11 +26,8 @@
 
 \<close>
 
-definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
-  where \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
-
 definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\<close>
+  where \<open>map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + 2 * drop_bit (Suc n) a)\<close>
 
 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>set_bit n = map_bit n top\<close>
@@ -42,11 +39,48 @@
   where \<open>flip_bit n = map_bit n Not\<close>
 
 text \<open>
-  The logical core are \<^const>\<open>bit\<close> and \<^const>\<open>map_bit\<close>; having 
+  Having 
   <^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
   operations allows to implement them using bit masks later.
 \<close>
 
+lemma stable_imp_drop_eq:
+  \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
+  by (induction n) (simp_all add: that)
+
+lemma map_bit_0 [simp]:
+  \<open>map_bit 0 f a = of_bool (f (odd a)) + 2 * (a div 2)\<close>
+  by (simp add: map_bit_def)
+
+lemma map_bit_Suc [simp]:
+  \<open>map_bit (Suc n) f a = a mod 2 + 2 * map_bit n f (a div 2)\<close>
+  by (auto simp add: map_bit_def algebra_simps mod2_eq_if push_bit_add mult_2
+    elim: evenE oddE)
+
+lemma set_bit_0 [simp]:
+  \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
+  by (simp add: set_bit_def)
+
+lemma set_bit_Suc [simp]:
+  \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
+  by (simp add: set_bit_def)
+
+lemma unset_bit_0 [simp]:
+  \<open>unset_bit 0 a = 2 * (a div 2)\<close>
+  by (simp add: unset_bit_def)
+
+lemma unset_bit_Suc [simp]:
+  \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
+  by (simp add: unset_bit_def)
+
+lemma flip_bit_0 [simp]:
+  \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
+  by (simp add: flip_bit_def)
+
+lemma flip_bit_Suc [simp]:
+  \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
+  by (simp add: flip_bit_def)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -126,7 +160,7 @@
   next
     case (even m)
     with rec [of "2 * m"] rec [of _ q] show ?case
-      by (cases "even n") (auto dest: False_P_imp)
+      by (cases "even n") (auto simp add: ac_simps dest: False_P_imp)
   next
     case (odd m)
     with rec [of "Suc (2 * m)"] rec [of _ q] show ?case

--- a/src/HOL/ex/Word.thy	Fri Nov 29 21:53:02 2019 +0100
+++ b/src/HOL/ex/Word.thy	Wed Nov 27 16:54:33 2019 +0000
@@ -277,7 +277,7 @@
 
 subsubsection \<open>Properties\<close>
 
-lemma length_cases:
+lemma length_cases: \<comment> \<open>TODO get rid of\<close>
   obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
     | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
 proof (cases "LENGTH('a) \<ge> 2")
@@ -569,15 +569,6 @@
 
 instance word :: (len) semiring_bits
 proof
-  show \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
-    for a b :: \<open>'a word\<close>
-    apply transfer
-    apply auto
-       apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod)
-      apply (metis even_take_bit_eq len_not_eq_0)
-     apply (metis even_take_bit_eq len_not_eq_0)
-    apply (metis (no_types, hide_lams) div_0 drop_bit_eq_div drop_bit_half dvd_mult_div_cancel even_take_bit_eq mod_div_trivial mod_eq_self_iff_div_eq_0 take_bit_eq_mod)
-    done
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
     and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
   for P and a :: \<open>'a word\<close>