# HG changeset patch
# User haftmann
# Date 1701032805 0
# Node ID 48ca09068adf226d4ab5ce38462581ea2bb8430d
# Parent  cb72e2c0c53965b7b6db1913ebef7f6de9b8c870
grouped lemmas for symbolic computations

diff -r cb72e2c0c539 -r 48ca09068adf src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Nov 26 21:06:43 2023 +0000
+++ b/src/HOL/Bit_Operations.thy	Sun Nov 26 21:06:45 2023 +0000
@@ -474,6 +474,10 @@
   \<open>possible_bit TYPE(nat) n\<close>
   by (simp add: possible_bit_def)
 
+lemma bit_Suc_0_iff [bit_simps]:
+  \<open>bit (Suc 0) n \<longleftrightarrow> n = 0\<close>
+  using bit_1_iff [of n, where ?'a = nat] by simp
+
 lemma not_bit_Suc_0_Suc [simp]:
   \<open>\<not> bit (Suc 0) (Suc n)\<close>
   by (simp add: bit_Suc)
@@ -2813,30 +2817,6 @@
   \<open>numeral (Num.Bit1 x) AND 1 = 1\<close>
   by (simp_all add: bit_eq_iff) (simp_all add: bit_0 bit_simps bit_Suc bit_numeral_rec split: nat.splits)
 
-fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<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>
-
-lemma numeral_and_num:
-  \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 | Some n' \<Rightarrow> numeral n')\<close>
-  by (induction m n rule: and_num.induct) (simp_all add: split: option.split)
-
-lemma and_num_eq_None_iff:
-  \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = 0\<close>
-  by (simp add: 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\<close>
-  by (simp add: numeral_and_num split: option.split)
-
 lemma or_numerals [simp]:
   \<open>1 OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
   \<open>1 OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\<close>
@@ -2848,26 +2828,6 @@
   \<open>numeral (Num.Bit1 x) OR 1 = numeral (Num.Bit1 x)\<close>
   by (simp_all add: bit_eq_iff) (simp_all add: bit_0 bit_simps bit_Suc bit_numeral_rec split: nat.splits)
 
-fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<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>
-
-lemma numeral_or_num:
-  \<open>numeral m OR numeral n = numeral (or_num m n)\<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\<close>
-  by (simp add: numeral_or_num)
-
 lemma xor_numerals [simp]:
   \<open>1 XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
   \<open>1 XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\<close>
@@ -2879,30 +2839,6 @@
   \<open>numeral (Num.Bit1 x) XOR 1 = numeral (Num.Bit0 x)\<close>
   by (simp_all add: bit_eq_iff) (simp_all add: bit_0 bit_simps bit_Suc bit_numeral_rec split: nat.splits)
 
-fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<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 numeral_xor_num:
-  \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 | 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\<close>
-  by (simp add: 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\<close>
-  by (simp add: numeral_xor_num split: option.split)
-
 end
 
 lemma drop_bit_Suc_minus_bit0 [simp]:
@@ -2937,10 +2873,6 @@
   \<open>take_bit (numeral l) (- numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
   by (simp add: numeral_eq_Suc numeral_Bit1_div_2 take_bit_Suc_minus_bit1)
 
-lemma bit_Suc_0_iff [bit_simps]:
-  \<open>bit (Suc 0) n \<longleftrightarrow> n = 0\<close>
-  using bit_1_iff [of n, where ?'a = nat] by simp
-
 lemma and_nat_numerals [simp]:
   \<open>Suc 0 AND numeral (Num.Bit0 y) = 0\<close>
   \<open>Suc 0 AND numeral (Num.Bit1 y) = 1\<close>
@@ -3219,6 +3151,176 @@
   take_bit_numeral_minus_numeral_int [simp]
 
 
+subsection \<open>Symbolic computations for code generation\<close>
+
+lemma bit_int_code [code]:
+  \<open>bit (0::int)               n      \<longleftrightarrow> False\<close>
+  \<open>bit (Int.Neg num.One)      n      \<longleftrightarrow> True\<close>
+  \<open>bit (Int.Pos num.One)      0      \<longleftrightarrow> True\<close>
+  \<open>bit (Int.Pos (num.Bit0 m)) 0      \<longleftrightarrow> False\<close>
+  \<open>bit (Int.Pos (num.Bit1 m)) 0      \<longleftrightarrow> True\<close>
+  \<open>bit (Int.Neg (num.Bit0 m)) 0      \<longleftrightarrow> False\<close>
+  \<open>bit (Int.Neg (num.Bit1 m)) 0      \<longleftrightarrow> True\<close>
+  \<open>bit (Int.Pos num.One)      (Suc n) \<longleftrightarrow> False\<close>
+  \<open>bit (Int.Pos (num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (Int.Pos m) n\<close>
+  \<open>bit (Int.Pos (num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (Int.Pos m) n\<close>
+  \<open>bit (Int.Neg (num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (Int.Neg m) n\<close>
+  \<open>bit (Int.Neg (num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (Int.Neg (Num.inc m)) n\<close>
+  by (simp_all add: Num.add_One bit_0 bit_Suc)
+
+lemma not_int_code [code]:
+  \<open>NOT (0 :: int) = - 1\<close>
+  \<open>NOT (Int.Pos n) = Int.Neg (Num.inc n)\<close>
+  \<open>NOT (Int.Neg n) = Num.sub n num.One\<close>
+  by (simp_all add: Num.add_One not_int_def)
+
+fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<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>
+
+context linordered_euclidean_semiring_bit_operations
+begin
+
+lemma numeral_and_num:
+  \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: and_num.induct) (simp_all add: split: option.split)
+
+lemma and_num_eq_None_iff:
+  \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = 0\<close>
+  by (simp add: 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\<close>
+  by (simp add: numeral_and_num split: option.split)
+
+end
+
+lemma and_int_code [code]:
+  fixes i j :: int shows
+  \<open>0 AND j = 0\<close>
+  \<open>i AND 0 = 0\<close>
+  \<open>Int.Pos n AND Int.Pos m = (case and_num n m of None \<Rightarrow> 0 | Some n' \<Rightarrow> Int.Pos n')\<close>
+  \<open>Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)\<close>
+  \<open>Int.Pos n AND Int.Neg num.One = Int.Pos n\<close>
+  \<open>Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (or_not_num_neg (Num.BitM m) n) num.One\<close>
+  \<open>Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (or_not_num_neg (num.Bit0 m) n) num.One\<close>
+  \<open>Int.Neg num.One AND Int.Pos m = Int.Pos m\<close>
+  \<open>Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (or_not_num_neg (Num.BitM n) m) num.One\<close>
+  \<open>Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (or_not_num_neg (num.Bit0 n) m) num.One\<close>
+  apply (auto simp add: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int]
+    split: option.split)
+     apply (simp_all only: sub_one_eq_not_neg numeral_or_not_num_eq minus_minus and_not_numerals
+       bit.de_Morgan_disj bit.double_compl and_not_num_eq_None_iff and_not_num_eq_Some_iff ac_simps)
+  done
+
+context linordered_euclidean_semiring_bit_operations
+begin
+
+fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<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>
+
+lemma numeral_or_num:
+  \<open>numeral m OR numeral n = numeral (or_num m n)\<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\<close>
+  by (simp add: numeral_or_num)
+
+end
+
+lemma or_int_code [code]:
+  fixes i j :: int shows
+  \<open>0 OR j = j\<close>
+  \<open>i OR 0 = i\<close>
+  \<open>Int.Pos n OR Int.Pos m = Int.Pos (or_num n m)\<close>
+  \<open>Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)\<close>
+  \<open>Int.Pos n OR Int.Neg num.One = Int.Neg num.One\<close>
+  \<open>Int.Pos n OR Int.Neg (num.Bit0 m) = (case and_not_num (Num.BitM m) n of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
+  \<open>Int.Pos n OR Int.Neg (num.Bit1 m) = (case and_not_num (num.Bit0 m) n of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
+  \<open>Int.Neg num.One OR Int.Pos m = Int.Neg num.One\<close>
+  \<open>Int.Neg (num.Bit0 n) OR Int.Pos m = (case and_not_num (Num.BitM n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
+  \<open>Int.Neg (num.Bit1 n) OR Int.Pos m = (case and_not_num (num.Bit0 n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
+  apply (auto simp add: numeral_or_num_eq split: option.splits)
+         apply (simp_all only: and_not_num_eq_None_iff and_not_num_eq_Some_iff and_not_numerals
+           numeral_or_not_num_eq or_eq_not_not_and bit.double_compl ac_simps flip: numeral_eq_iff [where ?'a = int])
+         apply simp_all
+  done
+
+fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<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>
+
+context linordered_euclidean_semiring_bit_operations
+begin
+
+lemma numeral_xor_num:
+  \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 | 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\<close>
+  by (simp add: 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\<close>
+  by (simp add: numeral_xor_num split: option.split)
+
+end
+
+lemma xor_int_code [code]:
+  fixes i j :: int shows
+  \<open>0 XOR j = j\<close>
+  \<open>i XOR 0 = i\<close>
+  \<open>Int.Pos n XOR Int.Pos m = (case xor_num n m of None \<Rightarrow> 0 | Some n' \<Rightarrow> Int.Pos n')\<close>
+  \<open>Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One\<close>
+  \<open>Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)\<close>
+  \<open>Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)\<close>
+  by (simp_all add: xor_num_eq_None_iff [where ?'a = int] xor_num_eq_Some_iff [where ?'a = int] split: option.split)
+
+lemma push_bit_int_code [code]:
+  \<open>push_bit 0 i = i\<close>
+  \<open>push_bit (Suc n) i = push_bit n (Int.dup i)\<close>
+  by (simp_all add: ac_simps)
+
+lemma drop_bit_int_code [code]:
+  fixes i :: int shows
+  \<open>drop_bit 0 i = i\<close>
+  \<open>drop_bit (Suc n) 0 = (0 :: int)\<close>
+  \<open>drop_bit (Suc n) (Int.Pos num.One) = 0\<close>
+  \<open>drop_bit (Suc n) (Int.Pos (num.Bit0 m)) = drop_bit n (Int.Pos m)\<close>
+  \<open>drop_bit (Suc n) (Int.Pos (num.Bit1 m)) = drop_bit n (Int.Pos m)\<close>
+  \<open>drop_bit (Suc n) (Int.Neg num.One) = - 1\<close>
+  \<open>drop_bit (Suc n) (Int.Neg (num.Bit0 m)) = drop_bit n (Int.Neg m)\<close>
+  \<open>drop_bit (Suc n) (Int.Neg (num.Bit1 m)) = drop_bit n (Int.Neg (Num.inc m))\<close>
+  by (simp_all add: drop_bit_Suc add_One)
+
+
 subsection \<open>More properties\<close>
 
 lemma take_bit_eq_mask_iff:
@@ -3625,93 +3727,6 @@
 qed
 
 
-subsection \<open>Symbolic computations for code generation\<close>
-
-lemma bit_int_code [code]:
-  \<open>bit (0::int)               n      \<longleftrightarrow> False\<close>
-  \<open>bit (Int.Neg num.One)      n      \<longleftrightarrow> True\<close>
-  \<open>bit (Int.Pos num.One)      0      \<longleftrightarrow> True\<close>
-  \<open>bit (Int.Pos (num.Bit0 m)) 0      \<longleftrightarrow> False\<close>
-  \<open>bit (Int.Pos (num.Bit1 m)) 0      \<longleftrightarrow> True\<close>
-  \<open>bit (Int.Neg (num.Bit0 m)) 0      \<longleftrightarrow> False\<close>
-  \<open>bit (Int.Neg (num.Bit1 m)) 0      \<longleftrightarrow> True\<close>
-  \<open>bit (Int.Pos num.One)      (Suc n) \<longleftrightarrow> False\<close>
-  \<open>bit (Int.Pos (num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (Int.Pos m) n\<close>
-  \<open>bit (Int.Pos (num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (Int.Pos m) n\<close>
-  \<open>bit (Int.Neg (num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (Int.Neg m) n\<close>
-  \<open>bit (Int.Neg (num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (Int.Neg (Num.inc m)) n\<close>
-  by (simp_all add: Num.add_One bit_0 bit_Suc)
-
-lemma not_int_code [code]:
-  \<open>NOT (0 :: int) = - 1\<close>
-  \<open>NOT (Int.Pos n) = Int.Neg (Num.inc n)\<close>
-  \<open>NOT (Int.Neg n) = Num.sub n num.One\<close>
-  by (simp_all add: Num.add_One not_int_def)
-
-lemma and_int_code [code]:
-  fixes i j :: int shows
-  \<open>0 AND j = 0\<close>
-  \<open>i AND 0 = 0\<close>
-  \<open>Int.Pos n AND Int.Pos m = (case and_num n m of None \<Rightarrow> 0 | Some n' \<Rightarrow> Int.Pos n')\<close>
-  \<open>Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)\<close>
-  \<open>Int.Pos n AND Int.Neg num.One = Int.Pos n\<close>
-  \<open>Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (or_not_num_neg (Num.BitM m) n) num.One\<close>
-  \<open>Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (or_not_num_neg (num.Bit0 m) n) num.One\<close>
-  \<open>Int.Neg num.One AND Int.Pos m = Int.Pos m\<close>
-  \<open>Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (or_not_num_neg (Num.BitM n) m) num.One\<close>
-  \<open>Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (or_not_num_neg (num.Bit0 n) m) num.One\<close>
-  apply (auto simp add: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int]
-    split: option.split)
-     apply (simp_all only: sub_one_eq_not_neg numeral_or_not_num_eq minus_minus and_not_numerals
-       bit.de_Morgan_disj bit.double_compl and_not_num_eq_None_iff and_not_num_eq_Some_iff ac_simps)
-  done
-
-lemma or_int_code [code]:
-  fixes i j :: int shows
-  \<open>0 OR j = j\<close>
-  \<open>i OR 0 = i\<close>
-  \<open>Int.Pos n OR Int.Pos m = Int.Pos (or_num n m)\<close>
-  \<open>Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)\<close>
-  \<open>Int.Pos n OR Int.Neg num.One = Int.Neg num.One\<close>
-  \<open>Int.Pos n OR Int.Neg (num.Bit0 m) = (case and_not_num (Num.BitM m) n of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
-  \<open>Int.Pos n OR Int.Neg (num.Bit1 m) = (case and_not_num (num.Bit0 m) n of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
-  \<open>Int.Neg num.One OR Int.Pos m = Int.Neg num.One\<close>
-  \<open>Int.Neg (num.Bit0 n) OR Int.Pos m = (case and_not_num (Num.BitM n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
-  \<open>Int.Neg (num.Bit1 n) OR Int.Pos m = (case and_not_num (num.Bit0 n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
-  apply (auto simp add: numeral_or_num_eq split: option.splits)
-         apply (simp_all only: and_not_num_eq_None_iff and_not_num_eq_Some_iff and_not_numerals
-           numeral_or_not_num_eq or_eq_not_not_and bit.double_compl ac_simps flip: numeral_eq_iff [where ?'a = int])
-         apply simp_all
-  done
-
-lemma xor_int_code [code]:
-  fixes i j :: int shows
-  \<open>0 XOR j = j\<close>
-  \<open>i XOR 0 = i\<close>
-  \<open>Int.Pos n XOR Int.Pos m = (case xor_num n m of None \<Rightarrow> 0 | Some n' \<Rightarrow> Int.Pos n')\<close>
-  \<open>Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One\<close>
-  \<open>Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)\<close>
-  \<open>Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)\<close>
-  by (simp_all add: xor_num_eq_None_iff [where ?'a = int] xor_num_eq_Some_iff [where ?'a = int] split: option.split)
-
-lemma push_bit_int_code [code]:
-  \<open>push_bit 0 i = i\<close>
-  \<open>push_bit (Suc n) i = push_bit n (Int.dup i)\<close>
-  by (simp_all add: ac_simps)
-
-lemma drop_bit_int_code [code]:
-  fixes i :: int shows
-  \<open>drop_bit 0 i = i\<close>
-  \<open>drop_bit (Suc n) 0 = (0 :: int)\<close>
-  \<open>drop_bit (Suc n) (Int.Pos num.One) = 0\<close>
-  \<open>drop_bit (Suc n) (Int.Pos (num.Bit0 m)) = drop_bit n (Int.Pos m)\<close>
-  \<open>drop_bit (Suc n) (Int.Pos (num.Bit1 m)) = drop_bit n (Int.Pos m)\<close>
-  \<open>drop_bit (Suc n) (Int.Neg num.One) = - 1\<close>
-  \<open>drop_bit (Suc n) (Int.Neg (num.Bit0 m)) = drop_bit n (Int.Neg m)\<close>
-  \<open>drop_bit (Suc n) (Int.Neg (num.Bit1 m)) = drop_bit n (Int.Neg (Num.inc m))\<close>
-  by (simp_all add: drop_bit_Suc add_One)
-
-
 subsection \<open>Key ideas of bit operations\<close>
 
 text \<open>