# HG changeset patch
# User haftmann
# Date 1594448462 0
# Node ID febdd4eead565d58a03512a2f2e1b861beafe838
# Parent  7a53fc156c2b6d3108bc9a8f8a809a83ac3eacc3
more on single-bit operations

diff -r 7a53fc156c2b -r febdd4eead56 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Fri Jul 10 22:38:03 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy	Sat Jul 11 06:21:02 2020 +0000
@@ -213,6 +213,14 @@
   \<open>a OR b = NOT (NOT a AND NOT b)\<close>
   by simp
 
+lemma not_add_distrib:
+  \<open>NOT (a + b) = NOT a - b\<close>
+  by (simp add: not_eq_complement algebra_simps)
+
+lemma not_diff_distrib:
+  \<open>NOT (a - b) = NOT a + b\<close>
+  using not_add_distrib [of a \<open>- b\<close>] by simp
+
 lemma push_bit_minus:
   \<open>push_bit n (- a) = - push_bit n a\<close>
   by (simp add: push_bit_eq_mult)
@@ -380,16 +388,20 @@
   qed
 qed
 
+lemma flip_bit_eq_if:
+  \<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close>
+  by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)
+
 lemma take_bit_set_bit_eq:
-  \<open>take_bit n (set_bit m w) = (if n \<le> m then take_bit n w else set_bit m (take_bit n w))\<close>
+  \<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close>
   by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff)
 
 lemma take_bit_unset_bit_eq:
-  \<open>take_bit n (unset_bit m w) = (if n \<le> m then take_bit n w else unset_bit m (take_bit n w))\<close>
+  \<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close>
   by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff)
 
 lemma take_bit_flip_bit_eq:
-  \<open>take_bit n (flip_bit m w) = (if n \<le> m then take_bit n w else flip_bit m (take_bit n w))\<close>
+  \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
   by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)
 
 end
@@ -501,6 +513,41 @@
 
 end
 
+lemma disjunctive_add:
+  \<open>k + l = k OR l\<close> if \<open>\<And>n. \<not> bit k n \<or> \<not> bit l n\<close> for k l :: int
+  \<comment> \<open>TODO: may integrate (indirectly) into \<^class>\<open>semiring_bits\<close> premises\<close>
+proof (rule bit_eqI)
+  fix n
+  from that have \<open>bit (k + l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
+  proof (induction n arbitrary: k l)
+    case 0
+    from this [of 0] show ?case
+      by auto
+  next
+    case (Suc n)
+    have \<open>bit ((k + l) div 2) n \<longleftrightarrow> bit (k div 2 + l div 2) n\<close>
+      using Suc.prems [of 0] div_add1_eq [of k l] by auto
+    also have \<open>bit (k div 2 + l div 2) n \<longleftrightarrow> bit (k div 2) n \<or> bit (l div 2) n\<close>
+      by (rule Suc.IH) (use Suc.prems in \<open>simp flip: bit_Suc\<close>)
+    finally show ?case
+      by (simp add: bit_Suc)
+  qed
+  also have \<open>\<dots> \<longleftrightarrow> bit (k OR l) n\<close>
+    by (simp add: bit_or_iff)
+  finally show \<open>bit (k + l) n \<longleftrightarrow> bit (k OR l) n\<close> .
+qed
+
+lemma disjunctive_diff:
+  \<open>k - l = k AND NOT l\<close> if \<open>\<And>n. bit l n \<Longrightarrow> bit k n\<close> for k l :: int
+proof -
+  have \<open>NOT k + l = NOT k OR l\<close>
+    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+  then have \<open>NOT (NOT k + l) = NOT (NOT k OR l)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: not_add_distrib)
+qed
+
 lemma not_nonnegative_int_iff [simp]:
   \<open>NOT k \<ge> 0 \<longleftrightarrow> k < 0\<close> for k :: int
   by (simp add: not_int_def)
@@ -538,6 +585,28 @@
   \<open>k AND l < 0 \<longleftrightarrow> k < 0 \<and> l < 0\<close> for k l :: int
   by (subst Not_eq_iff [symmetric]) (simp add: not_less)
 
+lemma and_less_eq:
+  \<open>k AND l \<le> k\<close> if \<open>l < 0\<close> for k l :: int
+using that proof (induction k arbitrary: l rule: int_bit_induct)
+  case zero
+  then show ?case
+    by simp
+next
+  case minus
+  then show ?case
+    by simp
+next
+  case (even k)
+  from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
+  show ?case
+    by (simp add: and_int_rec [of _ l])
+next
+  case (odd k)
+  from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
+  show ?case
+    by (simp add: and_int_rec [of _ l])
+qed
+
 lemma or_nonnegative_int_iff [simp]:
   \<open>k OR l \<ge> 0 \<longleftrightarrow> k \<ge> 0 \<and> l \<ge> 0\<close> for k l :: int
   by (simp only: or_eq_not_not_and not_nonnegative_int_iff) simp
@@ -546,6 +615,28 @@
   \<open>k OR l < 0 \<longleftrightarrow> k < 0 \<or> l < 0\<close> for k l :: int
   by (subst Not_eq_iff [symmetric]) (simp add: not_less)
 
+lemma or_greater_eq:
+  \<open>k OR l \<ge> k\<close> if \<open>l \<ge> 0\<close> for k l :: int
+using that proof (induction k arbitrary: l rule: int_bit_induct)
+  case zero
+  then show ?case
+    by simp
+next
+  case minus
+  then show ?case
+    by simp
+next
+  case (even k)
+  from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
+  show ?case
+    by (simp add: or_int_rec [of _ l])
+next
+  case (odd k)
+  from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
+  show ?case
+    by (simp add: or_int_rec [of _ l])
+qed
+
 lemma xor_nonnegative_int_iff [simp]:
   \<open>k XOR l \<ge> 0 \<longleftrightarrow> (k \<ge> 0 \<longleftrightarrow> l \<ge> 0)\<close> for k l :: int
   by (simp only: bit.xor_def or_nonnegative_int_iff) auto
@@ -578,50 +669,6 @@
   \<open>flip_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
   by (simp add: flip_bit_def)
 
-lemma and_less_eq:
-  \<open>k AND l \<le> k\<close> if \<open>l < 0\<close> for k l :: int
-using that proof (induction k arbitrary: l rule: int_bit_induct)
-  case zero
-  then show ?case
-    by simp
-next
-  case minus
-  then show ?case
-    by simp
-next
-  case (even k)
-  from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
-  show ?case
-    by (simp add: and_int_rec [of _ l])
-next
-  case (odd k)
-  from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
-  show ?case
-    by (simp add: and_int_rec [of _ l])
-qed
-
-lemma or_greater_eq:
-  \<open>k OR l \<ge> k\<close> if \<open>l \<ge> 0\<close> for k l :: int
-using that proof (induction k arbitrary: l rule: int_bit_induct)
-  case zero
-  then show ?case
-    by simp
-next
-  case minus
-  then show ?case
-    by simp
-next
-  case (even k)
-  from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
-  show ?case
-    by (simp add: or_int_rec [of _ l])
-next
-  case (odd k)
-  from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
-  show ?case
-    by (simp add: or_int_rec [of _ l])
-qed
-
 lemma set_bit_greater_eq:
   \<open>set_bit n k \<ge> k\<close> for k :: int
   by (simp add: set_bit_def or_greater_eq)
@@ -630,6 +677,52 @@
   \<open>unset_bit n k \<le> k\<close> for k :: int
   by (simp add: unset_bit_def and_less_eq)
 
+lemma set_bit_eq:
+  \<open>set_bit n k = k + of_bool (\<not> bit k n) * 2 ^ n\<close> for k :: int
+proof (rule bit_eqI)
+  fix m
+  show \<open>bit (set_bit n k) m \<longleftrightarrow> bit (k + of_bool (\<not> bit k n) * 2 ^ n) m\<close>
+  proof (cases \<open>m = n\<close>)
+    case True
+    then show ?thesis
+      apply (simp add: bit_set_bit_iff)
+      apply (simp add: bit_iff_odd div_plus_div_distrib_dvd_right)
+      done
+  next
+    case False
+    then show ?thesis
+      apply (clarsimp simp add: bit_set_bit_iff)
+      apply (subst disjunctive_add)
+      apply (clarsimp simp add: bit_exp_iff)
+      apply (clarsimp simp add: bit_or_iff bit_exp_iff)
+      done
+  qed
+qed
+
+lemma unset_bit_eq:
+  \<open>unset_bit n k = k - of_bool (bit k n) * 2 ^ n\<close> for k :: int
+proof (rule bit_eqI)
+  fix m
+  show \<open>bit (unset_bit n k) m \<longleftrightarrow> bit (k - of_bool (bit k n) * 2 ^ n) m\<close>
+  proof (cases \<open>m = n\<close>)
+    case True
+    then show ?thesis
+      apply (simp add: bit_unset_bit_iff)
+      apply (simp add: bit_iff_odd)
+      using div_plus_div_distrib_dvd_right [of \<open>2 ^ n\<close> \<open>- (2 ^ n)\<close> k]
+      apply (simp add: dvd_neg_div)
+      done
+  next
+    case False
+    then show ?thesis
+      apply (clarsimp simp add: bit_unset_bit_iff)
+      apply (subst disjunctive_diff)
+      apply (clarsimp simp add: bit_exp_iff)
+      apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff)
+      done
+  qed
+qed
+
 
 subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
diff -r 7a53fc156c2b -r febdd4eead56 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Jul 10 22:38:03 2020 +0200
+++ b/src/HOL/Word/Word.thy	Sat Jul 11 06:21:02 2020 +0000
@@ -919,6 +919,24 @@
 
 end
 
+context
+  includes lifting_syntax
+begin
+
+lemma set_bit_word_transfer:
+  \<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close>
+  by (unfold set_bit_def) transfer_prover
+
+lemma unset_bit_word_transfer:
+  \<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close>
+  by (unfold unset_bit_def) transfer_prover
+
+lemma flip_bit_word_transfer:
+  \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close>
+  by (unfold flip_bit_def) transfer_prover
+
+end
+
 instantiation word :: (len) semiring_bit_syntax
 begin