--- a/src/HOL/Code_Numeral.thy Tue Aug 03 13:53:22 2021 +0000
+++ b/src/HOL/Code_Numeral.thy Tue Aug 03 13:53:22 2021 +0000
@@ -293,12 +293,36 @@
instance integer :: unique_euclidean_ring_with_nat
by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
-instantiation integer :: semiring_bit_shifts
+instantiation integer :: ring_bit_operations
begin
lift_definition bit_integer :: \<open>integer \<Rightarrow> nat \<Rightarrow> bool\<close>
is bit .
+lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close>
+ is not .
+
+lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is \<open>and\<close> .
+
+lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is or .
+
+lift_definition xor_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is xor .
+
+lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close>
+ is mask .
+
+lift_definition set_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is set_bit .
+
+lift_definition unset_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is unset_bit .
+
+lift_definition flip_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is flip_bit .
+
lift_definition push_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
is push_bit .
@@ -312,18 +336,47 @@
(fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
- even_mask_div_iff even_mult_exp_div_exp_iff)+
+ even_mask_div_iff even_mult_exp_div_exp_iff
+ bit_and_iff bit_or_iff bit_xor_iff mask_eq_exp_minus_1
+ set_bit_def bit_unset_bit_iff flip_bit_def bit_not_iff minus_eq_not_minus_1)+
end
-instance integer :: unique_euclidean_semiring_with_bit_shifts ..
+instance integer :: unique_euclidean_semiring_with_bit_operations ..
+
+context
+ includes bit_operations_syntax
+begin
lemma [code]:
\<open>bit k n \<longleftrightarrow> odd (drop_bit n k)\<close>
+ \<open>NOT k = - k - 1\<close>
+ \<open>mask n = 2 ^ n - (1 :: integer)\<close>
+ \<open>set_bit n k = k OR push_bit n 1\<close>
+ \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close>
+ \<open>flip_bit n k = k XOR push_bit n 1\<close>
\<open>push_bit n k = k * 2 ^ n\<close>
\<open>drop_bit n k = k div 2 ^ n\<close>
\<open>take_bit n k = k mod 2 ^ n\<close> for k :: integer
- by (fact bit_iff_odd_drop_bit push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+ by (fact bit_iff_odd_drop_bit not_eq_complement mask_eq_exp_minus_1
+ set_bit_eq_or unset_bit_eq_and_not flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+
+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)
+
+end
instantiation integer :: unique_euclidean_semiring_numeral
begin
@@ -1018,12 +1071,33 @@
instance natural :: unique_euclidean_semiring_with_nat
by (standard; transfer) simp_all
-instantiation natural :: semiring_bit_shifts
+instantiation natural :: semiring_bit_operations
begin
lift_definition bit_natural :: \<open>natural \<Rightarrow> nat \<Rightarrow> bool\<close>
is bit .
+lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is \<open>and\<close> .
+
+lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is or .
+
+lift_definition xor_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is xor .
+
+lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close>
+ is mask .
+
+lift_definition set_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is set_bit .
+
+lift_definition unset_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is unset_bit .
+
+lift_definition flip_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is flip_bit .
+
lift_definition push_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
is push_bit .
@@ -1037,18 +1111,49 @@
(fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
- even_mask_div_iff even_mult_exp_div_exp_iff)+
+ even_mask_div_iff even_mult_exp_div_exp_iff bit_and_iff bit_or_iff bit_xor_iff
+ mask_eq_exp_minus_1 set_bit_def bit_unset_bit_iff flip_bit_def)+
end
-instance natural :: unique_euclidean_semiring_with_bit_shifts ..
+instance natural :: unique_euclidean_semiring_with_bit_operations ..
+
+context
+ includes bit_operations_syntax
+begin
lemma [code]:
\<open>bit m n \<longleftrightarrow> odd (drop_bit n m)\<close>
+ \<open>mask n = 2 ^ n - (1 :: integer)\<close>
+ \<open>set_bit n m = m OR push_bit n 1\<close>
+ \<open>flip_bit n m = m XOR push_bit n 1\<close>
\<open>push_bit n m = m * 2 ^ n\<close>
\<open>drop_bit n m = m div 2 ^ n\<close>
\<open>take_bit n m = m mod 2 ^ n\<close> for m :: natural
- by (fact bit_iff_odd_drop_bit push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+ by (fact bit_iff_odd_drop_bit mask_eq_exp_minus_1
+ set_bit_eq_or flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+
+lemma [code]:
+ \<open>m AND n = (if m = 0 \<or> n = 0 then 0
+ else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\<close> for m n :: natural
+ by transfer (fact and_nat_unfold)
+
+lemma [code]:
+ \<open>m OR n = (if m = 0 then n else if n = 0 then m
+ else max (m mod 2) (n mod 2) + 2 * ((m div 2) OR (n div 2)))\<close> for m n :: natural
+ by transfer (fact or_nat_unfold)
+
+lemma [code]:
+ \<open>m XOR n = (if m = 0 then n else if n = 0 then m
+ else (m mod 2 + n mod 2) mod 2 + 2 * ((m div 2) XOR (n div 2)))\<close> for m n :: natural
+ by transfer (fact xor_nat_unfold)
+
+lemma [code]:
+ \<open>unset_bit 0 m = 2 * (m div 2)\<close>
+ \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m :: natural
+ by (transfer; simp add: unset_bit_Suc)+
+
+end
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
@@ -1142,6 +1247,10 @@
"integer_of_natural (natural_of_integer k) = max 0 k"
by simp
+lemma [code]:
+ \<open>integer_of_natural (mask n) = mask n\<close>
+ by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
+
lemma [code_abbrev]:
"natural_of_integer (Code_Numeral.Pos k) = numeral k"
by transfer simp
@@ -1211,83 +1320,6 @@
"modulo :: natural \<Rightarrow> _"
integer_of_natural natural_of_integer
-
-subsection \<open>Bit operations\<close>
-
-instantiation integer :: ring_bit_operations
-begin
-
-lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close>
- is not .
-
-lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
- is \<open>and\<close> .
-
-lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
- is or .
-
-lift_definition xor_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
- is xor .
-
-lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close>
- is mask .
-
-lift_definition set_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
- is set_bit .
-
-lift_definition unset_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
- is unset_bit .
-
-lift_definition flip_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
- is flip_bit .
-
-instance by (standard; transfer)
- (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1
- bit_not_iff bit_and_iff bit_or_iff bit_xor_iff
- set_bit_def bit_unset_bit_iff flip_bit_def)
-
-end
-
-lemma [code]:
- \<open>mask n = 2 ^ n - (1::integer)\<close>
- by (simp add: mask_eq_exp_minus_1)
-
-instantiation natural :: semiring_bit_operations
-begin
-
-lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
- is \<open>and\<close> .
-
-lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
- is or .
-
-lift_definition xor_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
- is xor .
-
-lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close>
- is mask .
-
-lift_definition set_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
- is set_bit .
-
-lift_definition unset_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
- is unset_bit .
-
-lift_definition flip_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
- is flip_bit .
-
-instance by (standard; transfer)
- (simp_all add: mask_eq_exp_minus_1
- bit_and_iff bit_or_iff bit_xor_iff
- set_bit_def bit_unset_bit_iff flip_bit_def)
-
-end
-
-lemma [code]:
- \<open>integer_of_natural (mask n) = mask n\<close>
- by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
-
-
lifting_update integer.lifting
lifting_forget integer.lifting