--- a/src/HOL/Code_Numeral.thy Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/Code_Numeral.thy Sat Jun 20 05:56:28 2020 +0000
@@ -296,40 +296,34 @@
instantiation integer :: semiring_bit_shifts
begin
+lift_definition bit_integer :: \<open>integer \<Rightarrow> nat \<Rightarrow> bool\<close>
+ is bit .
+
lift_definition push_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
- is \<open>push_bit\<close> .
+ is push_bit .
lift_definition drop_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
- is \<open>drop_bit\<close> .
+ is drop_bit .
+
+lift_definition take_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+ is take_bit .
instance by (standard; transfer)
- (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+ (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)+
end
-context
- includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
- \<open>(pcr_integer ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
- by (unfold bit_def) transfer_prover
-
-lemma [transfer_rule]:
- \<open>((=) ===> pcr_integer ===> pcr_integer) take_bit take_bit\<close>
- by (unfold take_bit_eq_mod) transfer_prover
-
-end
-
instance integer :: unique_euclidean_semiring_with_bit_shifts ..
lemma [code]:
+ \<open>bit k n \<longleftrightarrow> odd (drop_bit n k)\<close>
\<open>push_bit n k = k * 2 ^ n\<close>
- \<open>drop_bit n k = k div 2 ^ n\<close> for k :: integer
- by (fact push_bit_eq_mult drop_bit_eq_div)+
+ \<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)+
instantiation integer :: unique_euclidean_semiring_numeral
begin
@@ -1027,40 +1021,34 @@
instantiation natural :: semiring_bit_shifts
begin
+lift_definition bit_natural :: \<open>natural \<Rightarrow> nat \<Rightarrow> bool\<close>
+ is bit .
+
lift_definition push_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
- is \<open>push_bit\<close> .
+ is push_bit .
lift_definition drop_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
- is \<open>drop_bit\<close> .
+ is drop_bit .
+
+lift_definition take_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+ is take_bit .
instance by (standard; transfer)
- (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+ (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)+
end
-context
- includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
- \<open>(pcr_natural ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
- by (unfold bit_def) transfer_prover
-
-lemma [transfer_rule]:
- \<open>((=) ===> pcr_natural ===> pcr_natural) take_bit take_bit\<close>
- by (unfold take_bit_eq_mod) transfer_prover
-
-end
-
instance natural :: unique_euclidean_semiring_with_bit_shifts ..
lemma [code]:
+ \<open>bit m n \<longleftrightarrow> odd (drop_bit n m)\<close>
\<open>push_bit n m = m * 2 ^ n\<close>
- \<open>drop_bit n m = m div 2 ^ n\<close> for m :: natural
- by (fact push_bit_eq_mult drop_bit_eq_div)+
+ \<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)+
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
--- a/src/HOL/Library/Bit_Operations.thy Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Sat Jun 20 05:56:28 2020 +0000
@@ -123,7 +123,7 @@
(simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2)
qed
-lemma take_bit_eq_mask [code]:
+lemma take_bit_eq_mask:
\<open>take_bit n a = a AND mask n\<close>
by (rule bit_eqI)
(auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
@@ -194,16 +194,14 @@
proof -
interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
apply standard
- apply (simp_all add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
- apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff)
+ apply (simp_all add: bit_eq_iff)
+ apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
done
show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
by standard
show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
- apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
- apply (simp_all add: bit_exp_iff, simp_all add: bit_def)
- apply (metis local.bit_exp_iff local.bits_div_by_0)
- apply (metis local.bit_exp_iff local.bits_div_by_0)
+ apply (simp add: fun_eq_iff bit_eq_iff bit.xor_def)
+ apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_xor_iff exp_eq_0_imp_not_bit)
done
qed
@@ -636,20 +634,6 @@
unbundle integer.lifting natural.lifting
-context
- includes lifting_syntax
-begin
-
-lemma transfer_rule_bit_integer [transfer_rule]:
- \<open>((pcr_integer :: int \<Rightarrow> integer \<Rightarrow> bool) ===> (=)) bit bit\<close>
- by (unfold bit_def) transfer_prover
-
-lemma transfer_rule_bit_natural [transfer_rule]:
- \<open>((pcr_natural :: nat \<Rightarrow> natural \<Rightarrow> bool) ===> (=)) bit bit\<close>
- by (unfold bit_def) transfer_prover
-
-end
-
instantiation integer :: ring_bit_operations
begin
@@ -742,7 +726,7 @@
beyond the boundary. The property \<^prop>\<open>(2 :: int) ^ n \<noteq> 0\<close>
represents that \<^term>\<open>n\<close> is \<^emph>\<open>not\<close> beyond that boundary.
- \<^item> The projection on a single bit is then @{thm bit_def [where ?'a = int, no_vars]}.
+ \<^item> The projection on a single bit is then @{thm bit_iff_odd [where ?'a = int, no_vars]}.
\<^item> This leads to the most fundamental properties of bit values:
--- a/src/HOL/Library/Z2.thy Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/Library/Z2.thy Sat Jun 20 05:56:28 2020 +0000
@@ -194,15 +194,19 @@
end
-instance bit :: semiring_bits
+instantiation bit :: semiring_bits
+begin
+
+definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close>
+ where [simp]: \<open>bit_bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close>
+
+instance
apply standard
- apply (auto simp add: power_0_left power_add)
- apply (metis bit_not_1_iff of_bool_eq(2))
+ apply (auto simp add: power_0_left power_add set_iff)
+ apply (metis bit_not_1_iff of_bool_eq(2))
done
-lemma bit_bit_iff [simp]:
- \<open>bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close> for b :: bit
- by (cases b; cases n) (simp_all add: bit_Suc)
+end
instantiation bit :: semiring_bit_shifts
begin
@@ -213,8 +217,11 @@
definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
where \<open>drop_bit n b = (if n = 0 then b else 0)\<close> for b :: bit
+definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+ where \<open>take_bit n b = (if n = 0 then 0 else b)\<close> for b :: bit
+
instance
- by standard (simp_all add: push_bit_bit_def drop_bit_bit_def)
+ by standard (simp_all add: push_bit_bit_def drop_bit_bit_def take_bit_bit_def)
end
--- a/src/HOL/Parity.thy Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/Parity.thy Sat Jun 20 05:56:28 2020 +0000
@@ -727,8 +727,16 @@
and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
and even_mult_exp_div_exp_iff: \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> m > n \<or> 2 ^ n = 0 \<or> (m \<le> n \<and> even (a div 2 ^ (n - m)))\<close>
+ fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
+ assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
begin
+text \<open>
+ Having \<^const>\<open>bit\<close> as definitional class operation
+ takes into account that specific instances can be implemented
+ differently wrt. code generation.
+\<close>
+
lemma bits_div_by_0 [simp]:
\<open>a div 0 = 0\<close>
by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
@@ -782,16 +790,13 @@
\<open>1 mod 2 = 1\<close>
by (simp add: mod2_eq_if)
-definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
- where \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
-
lemma bit_0 [simp]:
\<open>bit a 0 \<longleftrightarrow> odd a\<close>
- by (simp add: bit_def)
+ by (simp add: bit_iff_odd)
lemma bit_Suc:
\<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
- using div_exp_eq [of a 1 n] by (simp add: bit_def)
+ using div_exp_eq [of a 1 n] by (simp add: bit_iff_odd)
lemma bit_rec:
\<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
@@ -799,7 +804,7 @@
lemma bit_0_eq [simp]:
\<open>bit 0 = bot\<close>
- by (simp add: fun_eq_iff bit_def)
+ by (simp add: fun_eq_iff bit_iff_odd)
context
fixes a
@@ -850,7 +855,7 @@
lemma exp_eq_0_imp_not_bit:
\<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
- using that by (simp add: bit_def)
+ using that by (simp add: bit_iff_odd)
lemma bit_eqI:
\<open>a = b\<close> if \<open>\<And>n. 2 ^ n \<noteq> 0 \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
@@ -912,7 +917,7 @@
lemma bit_exp_iff:
\<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
- by (auto simp add: bit_def exp_div_exp_eq)
+ by (auto simp add: bit_iff_odd exp_div_exp_eq)
lemma bit_1_iff:
\<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
@@ -924,7 +929,7 @@
lemma even_bit_succ_iff:
\<open>bit (1 + a) n \<longleftrightarrow> bit a n \<or> n = 0\<close> if \<open>even a\<close>
- using that by (cases \<open>n = 0\<close>) (simp_all add: bit_def)
+ using that by (cases \<open>n = 0\<close>) (simp_all add: bit_iff_odd)
lemma odd_bit_iff_bit_pred:
\<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close>
@@ -938,7 +943,7 @@
lemma bit_double_iff:
\<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close>
using even_mult_exp_div_exp_iff [of a 1 n]
- by (cases n, auto simp add: bit_def ac_simps)
+ by (cases n, auto simp add: bit_iff_odd ac_simps)
lemma bit_eq_rec:
\<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
@@ -970,11 +975,11 @@
lemma bit_mod_2_iff [simp]:
\<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
- by (cases a rule: parity_cases) (simp_all add: bit_def)
+ by (cases a rule: parity_cases) (simp_all add: bit_iff_odd)
lemma bit_mask_iff:
\<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
- by (simp add: bit_def even_mask_div_iff not_le)
+ by (simp add: bit_iff_odd even_mask_div_iff not_le)
lemma bit_Numeral1_iff [simp]:
\<open>bit (numeral Num.One) n \<longleftrightarrow> n = 0\<close>
@@ -1011,7 +1016,13 @@
qed
qed
-instance nat :: semiring_bits
+instantiation nat :: semiring_bits
+begin
+
+definition bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> bool\<close>
+ where \<open>bit_nat m n \<longleftrightarrow> odd (m div 2 ^ n)\<close>
+
+instance
proof
show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
@@ -1048,7 +1059,9 @@
apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc)
done
-qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff bit_nat_def)
+
+end
lemma int_bit_induct [case_names zero minus even odd]:
"P k" if zero_int: "P 0"
@@ -1107,7 +1120,13 @@
qed
qed
-instance int :: semiring_bits
+instantiation int :: semiring_bits
+begin
+
+definition bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
+ where \<open>bit_int k n \<longleftrightarrow> odd (k div 2 ^ n)\<close>
+
+instance
proof
show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
@@ -1169,18 +1188,19 @@
apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2))
done
-qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le bit_int_def)
+
+end
class semiring_bit_shifts = semiring_bits +
fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
+ fixes take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+ assumes take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
begin
-definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
- where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
-
text \<open>
Logically, \<^const>\<open>push_bit\<close>,
\<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
@@ -1188,14 +1208,14 @@
would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
algebraic relationships between those operations.
Having
- \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations
+ them as definitional class operations
takes into account that specific instances of these can be implemented
differently wrt. code generation.
\<close>
lemma bit_iff_odd_drop_bit:
\<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
- by (simp add: bit_def drop_bit_eq_div)
+ by (simp add: bit_iff_odd drop_bit_eq_div)
lemma even_drop_bit_iff_not_bit:
\<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
@@ -1359,15 +1379,15 @@
lemma bit_push_bit_iff:
\<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> (n < m \<or> bit a (n - m))\<close>
- by (auto simp add: bit_def push_bit_eq_mult even_mult_exp_div_exp_iff)
+ by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
lemma bit_drop_bit_eq:
\<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
- by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div)
+ by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
lemma bit_take_bit_iff:
\<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
- by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div)
+ by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)
lemma stable_imp_drop_bit_eq:
\<open>drop_bit n a = a\<close>
@@ -1419,12 +1439,11 @@
definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
-instance proof
- show \<open>push_bit n m = m * 2 ^ n\<close> for n m :: nat
- by (simp add: push_bit_nat_def)
- show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
- by (simp add: drop_bit_nat_def)
-qed
+definition take_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+ where \<open>take_bit_nat n m = m mod 2 ^ n\<close>
+
+instance
+ by standard (simp_all add: push_bit_nat_def drop_bit_nat_def take_bit_nat_def)
end
@@ -1437,12 +1456,11 @@
definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>drop_bit_int n k = k div 2 ^ n\<close>
-instance proof
- show \<open>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
- by (simp add: push_bit_int_def)
- show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
- by (simp add: drop_bit_int_def)
-qed
+definition take_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>take_bit_int n k = k mod 2 ^ n\<close>
+
+instance
+ by standard (simp_all add: push_bit_int_def drop_bit_int_def take_bit_int_def)
end
@@ -1538,7 +1556,7 @@
also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
by (simp add: of_nat_div)
finally show ?thesis
- by (simp add: bit_def semiring_bits_class.bit_def)
+ by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
qed
lemma of_nat_push_bit:
--- a/src/HOL/Word/Word.thy Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/Word/Word.thy Sat Jun 20 05:56:28 2020 +0000
@@ -662,8 +662,29 @@
(auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
-instance word :: (len) semiring_bits
+instantiation word :: (len) semiring_bits
+begin
+
+lift_definition bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close>
+ is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close>
proof
+ fix k l :: int and n :: nat
+ assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+ show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close>
+ proof (cases \<open>n < LENGTH('a)\<close>)
+ case True
+ from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close>
+ by simp
+ then show ?thesis
+ by (simp add: bit_take_bit_iff)
+ next
+ case False
+ then show ?thesis
+ by simp
+ qed
+qed
+
+instance proof
show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
for P and a :: \<open>'a word\<close>
@@ -682,6 +703,8 @@
with rec [of a True] show ?case
using bit_word_half_eq [of a True] by (simp add: ac_simps)
qed
+ show \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n
+ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit)
show \<open>0 div a = 0\<close>
for a :: \<open>'a word\<close>
by transfer simp
@@ -747,21 +770,6 @@
qed
qed
-context
- includes lifting_syntax
-begin
-
-lemma transfer_rule_bit_word [transfer_rule]:
- \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
-proof -
- let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
- have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
- by (unfold bit_def) transfer_prover
- also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
- by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
- finally show ?thesis .
-qed
-
end
instantiation word :: (len) semiring_bit_shifts
@@ -788,11 +796,17 @@
is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
by (simp add: take_bit_eq_mod)
+lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
+ by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
+
instance proof
- show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
+ show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
by transfer (simp add: push_bit_eq_mult)
- show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
+ show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
+ show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
+ by transfer (auto simp flip: take_bit_eq_mod)
qed
end
@@ -916,6 +930,10 @@
\<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close>
by (simp add: shiftr_word_eq)
+lemma [code]:
+ \<open>take_bit n a = a AND Bit_Operations.mask n\<close> for a :: \<open>'a::len word\<close>
+ by (fact take_bit_eq_mask)
+
lemma [code_abbrev]:
\<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
by (fact push_bit_of_1)
@@ -944,12 +962,9 @@
\<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def)
-definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
- where [code_abbrev]: \<open>bit_word = bit\<close>
-
-lemma bit_word_iff [code]:
- \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
- by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
+lemma bit_word_iff_drop_bit_and [code]:
+ \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
+ by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
subsection \<open>Shift operations\<close>
--- a/src/HOL/ex/Word.thy Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/ex/Word.thy Sat Jun 20 05:56:28 2020 +0000
@@ -548,8 +548,29 @@
(auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
-instance word :: (len) semiring_bits
+instantiation word :: (len) semiring_bits
+begin
+
+lift_definition bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close>
+ is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close>
proof
+ fix k l :: int and n :: nat
+ assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+ show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close>
+ proof (cases \<open>n < LENGTH('a)\<close>)
+ case True
+ from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close>
+ by simp
+ then show ?thesis
+ by (simp add: bit_take_bit_iff)
+ next
+ case False
+ then show ?thesis
+ by simp
+ qed
+qed
+
+instance proof
show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
for P and a :: \<open>'a word\<close>
@@ -566,6 +587,8 @@
with rec [of a True] show ?case
using bit_word_half_eq [of a True] by (simp add: ac_simps)
qed
+ show \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n
+ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit)
show \<open>0 div a = 0\<close>
for a :: \<open>'a word\<close>
by transfer simp
@@ -631,21 +654,6 @@
qed
qed
-context
- includes lifting_syntax
-begin
-
-lemma transfer_rule_bit_word [transfer_rule]:
- \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
-proof -
- let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
- have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
- by (unfold bit_def) transfer_prover
- also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
- by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
- finally show ?thesis .
-qed
-
end
instantiation word :: (len) semiring_bit_shifts
@@ -672,11 +680,17 @@
is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
by (simp add: take_bit_eq_mod)
+lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
+ by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
+
instance proof
show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
by transfer (simp add: push_bit_eq_mult)
show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
+ show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
+ by transfer (auto simp flip: take_bit_eq_mod)
qed
end
@@ -723,12 +737,9 @@
\<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
by (simp add: even_word_def and_one_eq even_iff_mod_2_eq_zero)
-definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
- where [code_abbrev]: \<open>bit_word = bit\<close>
-
-lemma bit_word_iff [code]:
- \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
- by (simp add: bit_word_def bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)
+lemma bit_word_iff_drop_bit_and [code]:
+ \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
+ by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
lifting_update word.lifting
lifting_forget word.lifting