# HG changeset patch
# User haftmann
# Date 1626090062 0
# Node ID ca2a35c0fe6e9e2c5c5a359e1bdbb3ca83b7fc73
# Parent  0274d442b7eac7e92d148063aada10f108ddea02
operations for symbolic computation of bit operations

diff -r 0274d442b7ea -r ca2a35c0fe6e src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Mon Jul 12 11:41:02 2021 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Mon Jul 12 11:41:02 2021 +0000
@@ -58,35 +58,35 @@
   using bit_xor_iff [of a b 0] by auto
 
 lemma zero_and_eq [simp]:
-  "0 AND a = 0"
+  \<open>0 AND a = 0\<close>
   by (simp add: bit_eq_iff bit_and_iff)
 
 lemma and_zero_eq [simp]:
-  "a AND 0 = 0"
+  \<open>a AND 0 = 0\<close>
   by (simp add: bit_eq_iff bit_and_iff)
 
 lemma one_and_eq:
-  "1 AND a = a mod 2"
+  \<open>1 AND a = a mod 2\<close>
   by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
 
 lemma and_one_eq:
-  "a AND 1 = a mod 2"
+  \<open>a AND 1 = a mod 2\<close>
   using one_and_eq [of a] by (simp add: ac_simps)
 
 lemma one_or_eq:
-  "1 OR a = a + of_bool (even a)"
+  \<open>1 OR a = a + of_bool (even a)\<close>
   by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)
 
 lemma or_one_eq:
-  "a OR 1 = a + of_bool (even a)"
+  \<open>a OR 1 = a + of_bool (even a)\<close>
   using one_or_eq [of a] by (simp add: ac_simps)
 
 lemma one_xor_eq:
-  "1 XOR a = a + of_bool (even a) - of_bool (odd a)"
+  \<open>1 XOR a = a + of_bool (even a) - of_bool (odd a)\<close>
   by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE)
 
 lemma xor_one_eq:
-  "a XOR 1 = a + of_bool (even a) - of_bool (odd a)"
+  \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
   using one_xor_eq [of a] by (simp add: ac_simps)
 
 lemma take_bit_and [simp]:
@@ -370,7 +370,7 @@
   by (simp add: minus_eq_not_minus_1 bit_not_iff)
 
 lemma even_not_iff [simp]:
-  "even (NOT a) \<longleftrightarrow> odd a"
+  \<open>even (NOT a) \<longleftrightarrow> odd a\<close>
   using bit_not_iff [of a 0] by auto
 
 lemma bit_not_exp_iff [bit_simps]:
@@ -390,7 +390,7 @@
   by (simp add: bit_minus_iff bit_1_iff)
 
 lemma not_one [simp]:
-  "NOT 1 = - 2"
+  \<open>NOT 1 = - 2\<close>
   by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
 
 sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
@@ -468,7 +468,7 @@
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
 
 lemma take_bit_not_iff:
-  "take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b"
+  \<open>take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b\<close>
   apply (simp add: bit_eq_iff)
   apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
   apply (use exp_eq_0_imp_not_bit in blast)
@@ -599,7 +599,7 @@
   where \<open>not_int k = - k - 1\<close>
 
 lemma not_int_rec:
-  "NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+  \<open>NOT k = of_bool (even k) + 2 * NOT (k div 2)\<close> for k :: int
   by (auto simp add: not_int_def elim: oddE)
 
 lemma even_not_iff_int:
@@ -828,8 +828,8 @@
 
 lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
-  shows "x OR y < 2 ^ n"
+  assumes \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close>
+  shows \<open>x OR y < 2 ^ n\<close>
 using assms proof (induction x arbitrary: y n rule: int_bit_induct)
   case zero
   then show ?case
@@ -852,8 +852,8 @@
 
 lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
-  shows "x XOR y < 2 ^ n"
+  assumes \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close>
+  shows \<open>x XOR y < 2 ^ n\<close>
 using assms proof (induction x arbitrary: y n rule: int_bit_induct)
   case zero
   then show ?case
@@ -876,26 +876,26 @@
 
 lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> x"
-  shows "0 \<le> x AND y"
+  assumes \<open>0 \<le> x\<close>
+  shows \<open>0 \<le> x AND y\<close>
   using assms by simp
 
 lemma OR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> x" "0 \<le> y"
-  shows "0 \<le> x OR y"
+  assumes \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
+  shows \<open>0 \<le> x OR y\<close>
   using assms by simp
 
 lemma XOR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> x" "0 \<le> y"
-  shows "0 \<le> x XOR y"
+  assumes \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
+  shows \<open>0 \<le> x XOR y\<close>
   using assms by simp
 
 lemma AND_upper1 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> x"
-  shows "x AND y \<le> x"
+  assumes \<open>0 \<le> x\<close>
+  shows \<open>x AND y \<le> x\<close>
 using assms proof (induction x arbitrary: y rule: int_bit_induct)
   case (odd k)
   then have \<open>k AND y div 2 \<le> k\<close>
@@ -909,8 +909,8 @@
 
 lemma AND_upper2 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   fixes x y :: int
-  assumes "0 \<le> y"
-  shows "x AND y \<le> y"
+  assumes \<open>0 \<le> y\<close>
+  shows \<open>x AND y \<le> y\<close>
   using assms AND_upper1 [of y x] by (simp add: ac_simps)
 
 lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
@@ -1118,6 +1118,22 @@
 
 end
 
+lemma minus_numeral_inc_eq:
+  \<open>- numeral (Num.inc n) = NOT (numeral n :: int)\<close>
+  by (simp add: not_int_def sub_inc_One_eq add_One)
+
+lemma sub_one_eq_not_neg:
+  \<open>Num.sub n num.One = NOT (- numeral n :: int)\<close>
+  by (simp add: not_int_def)
+
+lemma int_not_numerals [simp]:
+  \<open>NOT (numeral (Num.Bit0 n) :: int) = - numeral (Num.Bit1 n)\<close>
+  \<open>NOT (numeral (Num.Bit1 n) :: int) = - numeral (Num.inc (num.Bit1 n))\<close>
+  \<open>NOT (numeral (Num.BitM n) :: int) = - numeral (num.Bit0 n)\<close>
+  \<open>NOT (- numeral (Num.Bit0 n) :: int) = numeral (Num.BitM n)\<close>
+  \<open>NOT (- numeral (Num.Bit1 n) :: int) = numeral (Num.Bit0 n)\<close>
+  by (simp_all add: not_int_def add_One inc_BitM_eq) 
+
 text \<open>FIXME: The rule sets below are very large (24 rules for each
   operator). Is there a simpler way to do this?\<close>
 
@@ -1144,84 +1160,84 @@
 qed
 
 lemma int_and_numerals [simp]:
-  "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
-  "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)"
-  "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
-  "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)"
-  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
-  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))"
-  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
-  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))"
-  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)"
-  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)"
-  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
-  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
-  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)"
-  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))"
-  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)"
-  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))"
-  "(1::int) AND numeral (Num.Bit0 y) = 0"
-  "(1::int) AND numeral (Num.Bit1 y) = 1"
-  "(1::int) AND - numeral (Num.Bit0 y) = 0"
-  "(1::int) AND - numeral (Num.Bit1 y) = 1"
-  "numeral (Num.Bit0 x) AND (1::int) = 0"
-  "numeral (Num.Bit1 x) AND (1::int) = 1"
-  "- numeral (Num.Bit0 x) AND (1::int) = 0"
-  "- numeral (Num.Bit1 x) AND (1::int) = 1"
+  \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))\<close>
+  \<open>numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))\<close>
+  \<open>- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))\<close>
+  \<open>- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))\<close>
+  \<open>(1::int) AND numeral (Num.Bit0 y) = 0\<close>
+  \<open>(1::int) AND numeral (Num.Bit1 y) = 1\<close>
+  \<open>(1::int) AND - numeral (Num.Bit0 y) = 0\<close>
+  \<open>(1::int) AND - numeral (Num.Bit1 y) = 1\<close>
+  \<open>numeral (Num.Bit0 x) AND (1::int) = 0\<close>
+  \<open>numeral (Num.Bit1 x) AND (1::int) = 1\<close>
+  \<open>- numeral (Num.Bit0 x) AND (1::int) = 0\<close>
+  \<open>- numeral (Num.Bit1 x) AND (1::int) = 1\<close>
   by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI)
 
 lemma int_or_numerals [simp]:
-  "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)"
-  "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
-  "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
-  "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
-  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)"
-  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
-  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)"
-  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
-  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)"
-  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)"
-  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
-  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
-  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)"
-  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))"
-  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)"
-  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))"
-  "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
-  "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
-  "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
-  "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
-  "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
-  "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
-  "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
-  "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
+  \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\<close>
+  \<open>numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\<close>
+  \<open>- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))\<close>
+  \<open>- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))\<close>
+  \<open>(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
+  \<open>(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\<close>
+  \<open>(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\<close>
+  \<open>(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)\<close>
+  \<open>numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)\<close>
+  \<open>numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)\<close>
+  \<open>- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)\<close>
+  \<open>- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)\<close>
   by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
 
 lemma int_xor_numerals [simp]:
-  "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)"
-  "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
-  "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
-  "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)"
-  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)"
-  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
-  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)"
-  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
-  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)"
-  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)"
-  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
-  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
-  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)"
-  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))"
-  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)"
-  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))"
-  "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
-  "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
-  "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
-  "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
-  "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
-  "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
-  "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
-  "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
+  \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))\<close>
+  \<open>numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))\<close>
+  \<open>- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)\<close>
+  \<open>- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))\<close>
+  \<open>- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)\<close>
+  \<open>- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))\<close>
+  \<open>(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
+  \<open>(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\<close>
+  \<open>(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\<close>
+  \<open>(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))\<close>
+  \<open>numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)\<close>
+  \<open>numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)\<close>
+  \<open>- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)\<close>
+  \<open>- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))\<close>
   by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
 
 end
@@ -1621,10 +1637,6 @@
       (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
 qed
 
-lemma not_minus_numeral_inc_eq:
-  \<open>NOT (- numeral (Num.inc n)) = (numeral n :: int)\<close>
-  by (simp add: not_int_def sub_inc_One_eq)
-
 
 subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
@@ -1771,6 +1783,129 @@
 qed
 
 
+subsection \<open>Symbolic computations on numeral expressions\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+
+fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
+where
+  \<open>and_num num.One num.One = Some num.One\<close>
+| \<open>and_num num.One (num.Bit0 n) = None\<close>
+| \<open>and_num num.One (num.Bit1 n) = Some num.One\<close>
+| \<open>and_num (num.Bit0 m) num.One = None\<close>
+| \<open>and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit1 m) num.One = Some num.One\<close>
+| \<open>and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
+
+fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
+where
+  \<open>and_not_num num.One num.One = None\<close>
+| \<open>and_not_num num.One (num.Bit0 n) = Some num.One\<close>
+| \<open>and_not_num num.One (num.Bit1 n) = None\<close>
+| \<open>and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\<close>
+| \<open>and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
+| \<open>and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
+| \<open>and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
+
+fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close>
+where
+  \<open>or_num num.One num.One = num.One\<close>
+| \<open>or_num num.One (num.Bit0 n) = num.Bit1 n\<close>
+| \<open>or_num num.One (num.Bit1 n) = num.Bit1 n\<close>
+| \<open>or_num (num.Bit0 m) num.One = num.Bit1 m\<close>
+| \<open>or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\<close>
+| \<open>or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
+| \<open>or_num (num.Bit1 m) num.One = num.Bit1 m\<close>
+| \<open>or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\<close>
+| \<open>or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
+
+fun or_not_num_neg :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close>
+where
+  \<open>or_not_num_neg num.One num.One = num.One\<close>
+| \<open>or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\<close>
+| \<open>or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\<close>
+| \<open>or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\<close>
+| \<open>or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit1 n) num.One = num.One\<close>
+| \<open>or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\<close>
+
+fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
+where
+  \<open>xor_num num.One num.One = None\<close>
+| \<open>xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\<close>
+| \<open>xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\<close>
+| \<open>xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\<close>
+| \<open>xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\<close>
+| \<open>xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
+| \<open>xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
+| \<open>xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\<close>
+
+lemma int_numeral_and_num:
+  \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: and_num.induct) (simp_all split: option.split)
+
+lemma and_num_eq_None_iff:
+  \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = (0::int)\<close>
+  by (simp add: int_numeral_and_num split: option.split)
+
+lemma and_num_eq_Some_iff:
+  \<open>and_num m n = Some q \<longleftrightarrow> numeral m AND numeral n = (numeral q :: int)\<close>
+  by (simp add: int_numeral_and_num split: option.split)
+
+lemma int_numeral_and_not_num:
+  \<open>numeral m AND NOT (numeral n) = (case and_not_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: and_not_num.induct) (simp_all add: add_One BitM_inc_eq not_int_def split: option.split)
+
+lemma int_numeral_not_and_num:
+  \<open>NOT (numeral m) AND numeral n = (case and_not_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+  using int_numeral_and_not_num [of n m] by (simp add: ac_simps)
+
+lemma and_not_num_eq_None_iff:
+  \<open>and_not_num m n = None \<longleftrightarrow> numeral m AND NOT (numeral n) = (0::int)\<close>
+  by (simp add: int_numeral_and_not_num split: option.split)
+
+lemma and_not_num_eq_Some_iff:
+  \<open>and_not_num m n = Some q \<longleftrightarrow> numeral m AND NOT (numeral n) = (numeral q :: int)\<close>
+  by (simp add: int_numeral_and_not_num split: option.split)
+
+lemma int_numeral_or_num:
+  \<open>numeral m OR numeral n = (numeral (or_num m n) :: int)\<close>
+  by (induction m n rule: or_num.induct) simp_all
+
+lemma numeral_or_num_eq:
+  \<open>numeral (or_num m n) = (numeral m OR numeral n :: int)\<close>
+  by (simp add: int_numeral_or_num)
+
+lemma int_numeral_or_not_num_neg:
+  \<open>numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\<close>
+  by (induction m n rule: or_not_num_neg.induct) (simp_all add: add_One BitM_inc_eq not_int_def)
+
+lemma int_numeral_not_or_num_neg:
+  \<open>NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\<close>
+  using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps)
+
+lemma numeral_or_not_num_eq:
+  \<open>numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\<close>
+  using int_numeral_or_not_num_neg [of m n] by simp
+
+lemma int_numeral_xor_num:
+  \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: xor_num.induct) (simp_all split: option.split)
+
+lemma xor_num_eq_None_iff:
+  \<open>xor_num m n = None \<longleftrightarrow> numeral m XOR numeral n = (0::int)\<close>
+  by (simp add: int_numeral_xor_num split: option.split)
+
+lemma xor_num_eq_Some_iff:
+  \<open>xor_num m n = Some q \<longleftrightarrow> numeral m XOR numeral n = (numeral q :: int)\<close>
+  by (simp add: int_numeral_xor_num split: option.split)
+
+
 subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close>
 
 unbundle integer.lifting natural.lifting
diff -r 0274d442b7ea -r ca2a35c0fe6e src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Jul 12 11:41:02 2021 +0000
+++ b/src/HOL/Parity.thy	Mon Jul 12 11:41:02 2021 +0000
@@ -1584,6 +1584,10 @@
   qed
 qed
 
+lemma drop_bit_exp_eq:
+  \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> 2 ^ n \<noteq> 0) * 2 ^ (n - m)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
 end
 
 instantiation nat :: semiring_bit_shifts