# HG changeset patch
# User wenzelm
# Date 1736460377 -3600
# Node ID 1db8d9ee94ea6cc8106b5fb6ca00d6e599b6c3bf
# Parent  e7a77c795cf97a2f85226b94bff1484b53dc9edd# Parent  1609254b74c546669c875489ff96bde1203ac011
merged

diff -r 1609254b74c5 -r 1db8d9ee94ea src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Jan 09 14:53:05 2025 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Jan 09 23:06:17 2025 +0100
@@ -372,63 +372,6 @@
 
 instance integer :: linordered_euclidean_semiring_bit_operations ..
 
-context
-  includes bit_operations_syntax
-begin
-
-lemma [code]:
-  \<open>k AND l = (if k = 0 \<or> l = 0 then 0 else if k = - 1 then l else if l = - 1 then k
-    else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\<close> for k l :: integer
-  by transfer (fact and_int_unfold) 
-
-lemma [code]:
-  \<open>k OR l = (if k = - 1 \<or> l = - 1 then - 1 else if k = 0 then l else if l = 0 then k
-    else max (k mod 2) (l mod 2) + 2 * ((k div 2) OR (l div 2)))\<close> for k l :: integer
-  by transfer (fact or_int_unfold)
-
-lemma [code]:
-  \<open>k XOR l = (if k = - 1 then NOT l else if l = - 1 then NOT k else if k = 0 then l else if l = 0 then k
-    else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: integer
-  by transfer (fact xor_int_unfold)
-
-lemma [code]:
-  \<open>NOT k = - k - 1\<close> for k :: integer
-  by (fact not_eq_complement)
-
-lemma [code]:
-  \<open>bit k n \<longleftrightarrow> k AND push_bit n 1 \<noteq> (0 :: integer)\<close>
-  by (simp add: and_exp_eq_0_iff_not_bit)
-
-lemma [code]:
-  \<open>mask n = push_bit n 1 - (1 :: integer)\<close>
-  by (simp add: mask_eq_exp_minus_1)
-
-lemma [code]:
-  \<open>set_bit n k = k OR push_bit n 1\<close> for k :: integer
-  by (fact set_bit_def)
-
-lemma [code]:
-  \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close> for k :: integer
-  by (fact unset_bit_def)
-
-lemma [code]:
-  \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: integer
-  by (fact flip_bit_def)
-
-lemma [code]:
-  \<open>push_bit n k = k * 2 ^ n\<close> for k :: integer
-  by (fact push_bit_eq_mult)
-
-lemma [code]:
-  \<open>drop_bit n k = k div  2 ^ n\<close> for k :: integer
-  by (fact drop_bit_eq_div)
-
-lemma [code]:
-  \<open>take_bit n k = k AND mask n\<close> for k :: integer
-  by (fact take_bit_eq_mask)
-
-end
-
 instantiation integer :: linordered_euclidean_semiring_division
 begin
 
@@ -447,10 +390,6 @@
 
 end
 
-declare divmod_algorithm_code [where ?'a = integer,
-  folded integer_of_num_def, unfolded integer_of_num_triv,
-  code]
-
 lemma integer_of_nat_0: "integer_of_nat 0 = 0"
 by transfer simp
 
@@ -533,7 +472,7 @@
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
-  by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
+  by (transfer; simp only: numeral_Bit0 minus_add_distrib)+
 
 lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
   is "\<lambda>m n. numeral m - numeral n :: int"
@@ -549,7 +488,7 @@
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
-  by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
+  by (transfer; simp add: dbl_def dbl_inc_def dbl_dec_def)+
 
 
 text \<open>Implementations\<close>
@@ -623,6 +562,10 @@
   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
   by (simp add: divmod_abs_def)
 
+declare divmod_algorithm_code [where ?'a = integer,
+  folded integer_of_num_def, unfolded integer_of_num_triv,
+  code]
+
 lemma divmod_abs_code [code]:
   "divmod_abs (Pos k) (Pos l) = divmod k l"
   "divmod_abs (Neg k) (Neg l) = divmod k l"
@@ -653,13 +596,13 @@
   "divmod_integer k l =
    (if k = 0 then (0, 0)
     else if l > 0 then
-            (if k > 0 then Code_Numeral.divmod_abs k l
-             else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
+            (if k > 0 then divmod_abs k l
+             else case divmod_abs k l of (r, s) \<Rightarrow>
                   if s = 0 then (- r, 0) else (- r - 1, l - s))
     else if l = 0 then (0, k)
     else apsnd uminus
-            (if k < 0 then Code_Numeral.divmod_abs k l
-             else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
+            (if k < 0 then divmod_abs k l
+             else case divmod_abs k l of (r, s) \<Rightarrow>
                   if s = 0 then (- r, 0) else (- r - 1, - l - s)))"
   by (cases l "0 :: integer" rule: linorder_cases)
     (auto split: prod.splits simp add: divmod_integer_eq_cases)
@@ -672,6 +615,111 @@
   "k mod l = snd (divmod_integer k l)"
   by simp
 
+context
+  includes bit_operations_syntax
+begin
+
+lemma and_integer_code [code]:
+  \<open>Pos Num.One AND Pos Num.One = Pos Num.One\<close>
+  \<open>Pos Num.One AND Pos (Num.Bit0 n) = 0\<close>
+  \<open>Pos (Num.Bit0 m) AND Pos Num.One = 0\<close>
+  \<open>Pos Num.One AND Pos (Num.Bit1 n) = Pos Num.One\<close>
+  \<open>Pos (Num.Bit1 m) AND Pos Num.One = Pos Num.One\<close>
+  \<open>Pos (Num.Bit0 m) AND Pos (Num.Bit0 n) = dup (Pos m AND Pos n)\<close>
+  \<open>Pos (Num.Bit0 m) AND Pos (Num.Bit1 n) = dup (Pos m AND Pos n)\<close>
+  \<open>Pos (Num.Bit1 m) AND Pos (Num.Bit0 n) = dup (Pos m AND Pos n)\<close>
+  \<open>Pos (Num.Bit1 m) AND Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m AND Pos n)\<close>
+  \<open>Pos m AND Neg (num.Bit0 n) = (case and_not_num m (Num.BitM n) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close>
+  \<open>Neg (num.Bit0 m) AND Pos n = (case and_not_num n (Num.BitM m) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close>
+  \<open>Pos m AND Neg (num.Bit1 n) = (case and_not_num m (Num.Bit0 n) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close>
+  \<open>Neg (num.Bit1 m) AND Pos n = (case and_not_num n (Num.Bit0 m) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close>
+  \<open>Neg m AND Neg n = NOT (sub m Num.One OR sub n Num.One)\<close>
+  \<open>Neg Num.One AND k = k\<close>
+  \<open>k AND Neg Num.One = k\<close>
+  \<open>0 AND k = 0\<close>
+  \<open>k AND 0 = 0\<close>
+    for k :: integer
+  by (transfer; simp)+
+
+lemma or_integer_code [code]:
+  \<open>Pos Num.One AND Pos Num.One = Pos Num.One\<close>
+  \<open>Pos Num.One OR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)\<close>
+  \<open>Pos (Num.Bit0 m) OR Pos Num.One = Pos (Num.Bit1 m)\<close>
+  \<open>Pos Num.One OR Pos (Num.Bit1 n) = Pos (Num.Bit1 n)\<close>
+  \<open>Pos (Num.Bit1 m) OR Pos Num.One = Pos (Num.Bit1 m)\<close>
+  \<open>Pos (Num.Bit0 m) OR Pos (Num.Bit0 n) = dup (Pos m OR Pos n)\<close>
+  \<open>Pos (Num.Bit0 m) OR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m OR Pos n)\<close>
+  \<open>Pos (Num.Bit1 m) OR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m OR Pos n)\<close>
+  \<open>Pos (Num.Bit1 m) OR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m OR Pos n)\<close>
+  \<open>Pos m OR Neg (num.Bit0 n) = Neg (or_not_num_neg m (Num.BitM n))\<close>
+  \<open>Neg (num.Bit0 m) OR Pos n = Neg (or_not_num_neg n (Num.BitM m))\<close>
+  \<open>Pos m OR Neg (num.Bit1 n) = Neg (or_not_num_neg m (Num.Bit0 n))\<close>
+  \<open>Neg (num.Bit1 m) OR Pos n = Neg (or_not_num_neg n (Num.Bit0 m))\<close>
+  \<open>Neg m OR Neg n = NOT (sub m Num.One AND sub n Num.One)\<close>
+  \<open>Neg Num.One OR k = Neg Num.One\<close>
+  \<open>k OR Neg Num.One = Neg Num.One\<close>
+  \<open>0 OR k = k\<close>
+  \<open>k OR 0 = k\<close>
+    for k :: integer
+  by (transfer; simp)+
+
+lemma xor_integer_code [code]:
+  \<open>Pos Num.One XOR Pos Num.One = 0\<close>
+  \<open>Pos Num.One XOR numeral (Num.Bit0 n) = Pos (Num.Bit1 n)\<close>
+  \<open>Pos (Num.Bit0 m) XOR Pos Num.One = Pos (Num.Bit1 m)\<close>
+  \<open>Pos Num.One XOR numeral (Num.Bit1 n) = Pos (Num.Bit0 n)\<close>
+  \<open>Pos (Num.Bit1 m) XOR Pos Num.One = Pos (Num.Bit0 m)\<close>
+  \<open>Pos (Num.Bit0 m) XOR Pos (Num.Bit0 n) = dup (Pos m XOR Pos n)\<close>
+  \<open>Pos (Num.Bit0 m) XOR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m XOR Pos n)\<close>
+  \<open>Pos (Num.Bit1 m) XOR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m XOR Pos n)\<close>
+  \<open>Pos (Num.Bit1 m) XOR Pos (Num.Bit1 n) = dup (Pos m XOR Pos n)\<close>
+  \<open>Neg m XOR k = NOT (sub m num.One XOR k)\<close>
+  \<open>k XOR Neg n = NOT (k XOR (sub n num.One))\<close>
+  \<open>Neg Num.One XOR k = NOT k\<close>
+  \<open>k XOR Neg Num.One = NOT k\<close>
+  \<open>0 XOR k = k\<close>
+  \<open>k XOR 0 = k\<close>
+    for k :: integer
+  by (transfer; simp)+
+
+lemma [code]:
+  \<open>NOT k = - k - 1\<close> for k :: integer
+  by (fact not_eq_complement)
+
+lemma [code]:
+  \<open>bit k n \<longleftrightarrow> k AND push_bit n 1 \<noteq> (0 :: integer)\<close>
+  by (simp add: and_exp_eq_0_iff_not_bit)
+
+lemma [code]:
+  \<open>mask n = push_bit n 1 - (1 :: integer)\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma [code]:
+  \<open>set_bit n k = k OR push_bit n 1\<close> for k :: integer
+  by (fact set_bit_def)
+
+lemma [code]:
+  \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close> for k :: integer
+  by (fact unset_bit_def)
+
+lemma [code]:
+  \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: integer
+  by (fact flip_bit_def)
+
+lemma [code]:
+  \<open>push_bit n k = k * 2 ^ n\<close> for k :: integer
+  by (fact push_bit_eq_mult)
+
+lemma [code]:
+  \<open>drop_bit n k = k div  2 ^ n\<close> for k :: integer
+  by (fact drop_bit_eq_div)
+
+lemma [code]:
+  \<open>take_bit n k = k AND mask n\<close> for k :: integer
+  by (fact take_bit_eq_mask)
+
+end
+
 definition bit_cut_integer :: "integer \<Rightarrow> integer \<times> bool"
   where "bit_cut_integer k = (k div 2, odd k)"