--- a/src/HOL/Bit_Operations.thy Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Bit_Operations.thy Wed Feb 21 16:19:36 2024 +0000
@@ -14,9 +14,9 @@
\<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
\<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
\<Longrightarrow> P a\<close>
- assumes half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
+ assumes bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+ and half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close>
- and even_mod_exp_div_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<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
@@ -382,24 +382,6 @@
with rec [of n True] show ?case
by simp
qed
- show \<open>even (q mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (q div 2 ^ n)\<close> for q m n :: nat
- proof (cases \<open>m \<le> n\<close>)
- case True
- moreover define r where \<open>r = n - m\<close>
- ultimately have \<open>n = m + r\<close>
- by simp
- with True show ?thesis
- by (simp add: power_add div_mult2_eq)
- next
- case False
- moreover define r where \<open>r = m - Suc n\<close>
- ultimately have \<open>m = n + Suc r\<close>
- by simp
- moreover have \<open>even (q mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (q div 2 ^ n)\<close>
- by (simp only: power_add) (simp add: mod_mult2_eq dvd_mod_iff)
- ultimately show ?thesis
- by simp
- qed
qed (auto simp add: div_mult2_eq bit_nat_def)
end
@@ -539,24 +521,6 @@
with rec [of k True] show ?case
by (simp add: ac_simps)
qed
- show \<open>even (k mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (k div 2 ^ n)\<close> for k :: int and m n :: nat
- proof (cases \<open>m \<le> n\<close>)
- case True
- moreover define r where \<open>r = n - m\<close>
- ultimately have \<open>n = m + r\<close>
- by simp
- with True show ?thesis
- by (simp add: power_add zdiv_zmult2_eq)
- next
- case False
- moreover define r where \<open>r = m - Suc n\<close>
- ultimately have \<open>m = n + Suc r\<close>
- by simp
- moreover have \<open>even (k mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (k div 2 ^ n)\<close>
- by (simp only: power_add) (simp add: zmod_zmult2_eq dvd_mod_iff)
- ultimately show ?thesis
- by simp
- qed
qed (auto simp add: zdiv_zmult2_eq bit_int_def)
end
@@ -879,13 +843,96 @@
\<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
+lemma bit_drop_bit_eq [bit_simps]:
+ \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
+ by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
+
+lemma disjunctive_xor_eq_or:
+ \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
+ using that by (auto simp add: bit_eq_iff bit_simps)
+
+lemma disjunctive_add_eq_or:
+ \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>possible_bit TYPE('a) n\<close>
+ moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
+ by simp
+ then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+ by (simp add: bit_simps)
+ ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
+ proof (induction n arbitrary: a b)
+ case 0
+ from "0"(2)[of 0] show ?case
+ by (auto simp add: even_or_iff bit_0)
+ next
+ case (Suc n)
+ from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
+ by (auto simp add: bit_0)
+ have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+ using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+ from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
+ using possible_bit_less_imp by force
+ with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
+ have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+ by (simp add: bit_Suc)
+ have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+ using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+ also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+ using even by (auto simp add: algebra_simps mod2_eq_if)
+ finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+ using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
+ also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+ by (rule IH)
+ finally show ?case
+ by (simp add: bit_simps flip: bit_Suc)
+ qed
+qed
+
+lemma disjunctive_add_eq_xor:
+ \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
+ using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
+
lemma take_bit_0 [simp]:
"take_bit 0 a = 0"
by (simp add: take_bit_eq_mod)
lemma bit_take_bit_iff [bit_simps]:
\<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
- by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_div_exp_iff not_le)
+proof -
+ have \<open>push_bit m (drop_bit m a) AND take_bit m a = 0\<close> (is \<open>?lhs = _\<close>)
+ proof (rule bit_eqI)
+ fix n
+ show \<open>bit ?lhs n \<longleftrightarrow> bit 0 n\<close>
+ proof (cases \<open>m \<le> n\<close>)
+ case False
+ then show ?thesis
+ by (simp add: bit_simps)
+ next
+ case True
+ moreover define q where \<open>q = n - m\<close>
+ ultimately have \<open>n = m + q\<close> by simp
+ moreover have \<open>\<not> bit (take_bit m a) (m + q)\<close>
+ by (simp add: take_bit_eq_mod bit_iff_odd flip: div_exp_eq)
+ ultimately show ?thesis
+ by (simp add: bit_simps)
+ qed
+ qed
+ then have \<open>push_bit m (drop_bit m a) XOR take_bit m a = push_bit m (drop_bit m a) + take_bit m a\<close>
+ by (simp add: disjunctive_add_eq_xor)
+ also have \<open>\<dots> = a\<close>
+ by (simp add: bits_ident)
+ finally have \<open>bit (push_bit m (drop_bit m a) XOR take_bit m a) n \<longleftrightarrow> bit a n\<close>
+ by simp
+ also have \<open>\<dots> \<longleftrightarrow> (m \<le> n \<or> n < m) \<and> bit a n\<close>
+ by auto
+ also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
+ by auto
+ also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
+ by (auto simp add: bit_simps bit_imp_possible_bit)
+ finally show ?thesis
+ by (auto simp add: bit_simps)
+qed
lemma take_bit_Suc:
\<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
@@ -915,10 +962,6 @@
\<open>take_bit n 1 = of_bool (n > 0)\<close>
by (cases n) (simp_all add: take_bit_Suc)
-lemma bit_drop_bit_eq [bit_simps]:
- \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
- by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
-
lemma drop_bit_of_0 [simp]:
\<open>drop_bit n 0 = 0\<close>
by (rule bit_eqI) (simp add: bit_simps)
@@ -1245,52 +1288,6 @@
\<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
-lemma disjunctive_xor_eq_or:
- \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
- using that by (auto simp add: bit_eq_iff bit_simps)
-
-lemma disjunctive_add_eq_or:
- \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
-proof (rule bit_eqI)
- fix n
- assume \<open>possible_bit TYPE('a) n\<close>
- moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
- by simp
- then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
- by (simp add: bit_simps)
- ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
- proof (induction n arbitrary: a b)
- case 0
- from "0"(2)[of 0] show ?case
- by (auto simp add: even_or_iff bit_0)
- next
- case (Suc n)
- from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
- by (auto simp add: bit_0)
- have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
- using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
- from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
- using possible_bit_less_imp by force
- with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
- have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
- by (simp add: bit_Suc)
- have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
- using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
- also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
- using even by (auto simp add: algebra_simps mod2_eq_if)
- finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
- using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
- also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
- by (rule IH)
- finally show ?case
- by (simp add: bit_simps flip: bit_Suc)
- qed
-qed
-
-lemma disjunctive_add_eq_xor:
- \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
- using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
-
lemma set_bit_eq:
\<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
proof -
@@ -3921,6 +3918,10 @@
\<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
by (rule disjunctive_add_eq_or) (use that in \<open>simp add: bit_eq_iff bit_simps\<close>)
+lemma even_mod_exp_div_exp_iff [no_atp]:
+ \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
+ by (auto simp add: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod)
+
end
context ring_bit_operations
--- a/src/HOL/Code_Numeral.thy Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Code_Numeral.thy Wed Feb 21 16:19:36 2024 +0000
@@ -349,7 +349,7 @@
instance by (standard; transfer)
(fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
- half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
+ half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
and_rec or_rec xor_rec mask_eq_exp_minus_1
set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
@@ -1109,7 +1109,7 @@
instance by (standard; transfer)
(fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
- half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
+ half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
and_rec or_rec xor_rec mask_eq_exp_minus_1
set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
--- a/src/HOL/Library/Word.thy Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Library/Word.thy Wed Feb 21 16:19:36 2024 +0000
@@ -667,6 +667,32 @@
end
+lemma unat_div_distrib:
+ \<open>unat (v div w) = unat v div unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule div_le_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
+qed
+
+lemma unat_mod_distrib:
+ \<open>unat (v mod w) = unat v mod unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule mod_less_eq_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
+qed
+
instance word :: (len) semiring_parity
by (standard; transfer)
(auto simp add: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
@@ -838,6 +864,9 @@
show \<open>0 div a = 0\<close>
for a :: \<open>'a word\<close>
by transfer simp
+ show \<open>a mod b div b = 0\<close>
+ for a b :: \<open>'a word\<close>
+ by (simp add: word_eq_iff_unsigned [where ?'a = nat] unat_div_distrib unat_mod_distrib)
show \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
for a :: \<open>'a word\<close> and m n :: nat
apply transfer
@@ -849,10 +878,6 @@
for a :: \<open>'a word\<close> and n :: nat
using that by transfer
(simp add: even_drop_bit_iff_not_bit bit_simps flip: drop_bit_eq_div del: power.simps)
- show \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
- for a :: \<open>'a word\<close> and m n :: nat
- by transfer
- (auto simp flip: take_bit_eq_mod drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_simps)
qed
end
@@ -1301,32 +1326,6 @@
by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
(simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper)
-lemma unat_div_distrib:
- \<open>unat (v div w) = unat v div unat w\<close>
-proof transfer
- fix k l
- have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
- by (rule div_le_dividend)
- also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
- by (simp add: nat_less_iff)
- finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
- (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
-qed
-
-lemma unat_mod_distrib:
- \<open>unat (v mod w) = unat v mod unat w\<close>
-proof transfer
- fix k l
- have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
- by (rule mod_less_eq_dividend)
- also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
- by (simp add: nat_less_iff)
- finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
- (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
-qed
-
lemma uint_div_distrib:
\<open>uint (v div w) = uint v div uint w\<close>
proof -