--- a/src/HOL/Bit_Operations.thy Fri Jan 26 11:19:22 2024 +0000
+++ b/src/HOL/Bit_Operations.thy Fri Jan 26 11:19:30 2024 +0000
@@ -5,7 +5,7 @@
theory Bit_Operations
imports Presburger Groups_List
-begin
+begin
subsection \<open>Abstract bit structures\<close>
@@ -14,17 +14,14 @@
\<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 bits_div_0 [simp]: \<open>0 div a = 0\<close>
- and bits_div_by_0 [simp]: \<open>a div 0 = 0\<close>
+ assumes bits_div_by_0 [simp]: \<open>a div 0 = 0\<close>
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
+ and bits_0_div [simp]: \<open>0 div a = 0\<close>
and even_half_succ_eq [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
- and even_mask_div_iff: \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
- and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
- and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
- and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
- 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>
+ 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_decr_exp_div_exp_iff: \<open>2 ^ n \<noteq> 0 \<Longrightarrow> even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
+ and even_mod_exp_diff_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
@@ -35,64 +32,36 @@
differently wrt. code generation.
\<close>
-lemma bits_1_div_2 [simp]:
+lemma half_1 [simp]:
\<open>1 div 2 = 0\<close>
using even_half_succ_eq [of 0] by simp
-lemma bits_1_div_exp [simp]:
- \<open>1 div 2 ^ n = of_bool (n = 0)\<close>
- using div_exp_eq [of 1 1] by (cases n) simp_all
-
-lemma even_succ_div_exp [simp]:
- \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close>
-proof (cases n)
- case 0
- with that show ?thesis
- by simp
-next
- case (Suc n)
- with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close>
- proof (induction n)
- case 0
- then show ?case
- by simp
- next
- case (Suc n)
- then show ?case
- using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric]
- by simp
- qed
- with Suc show ?thesis
- by simp
-qed
-
-lemma even_succ_mod_exp [simp]:
- \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
- using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
- by simp (metis (full_types) add.left_commute add_left_imp_eq)
+lemma bits_mod_by_0 [simp]:
+ \<open>a mod 0 = a\<close>
+ using div_mult_mod_eq [of a 0] by simp
lemma bits_mod_by_1 [simp]:
\<open>a mod 1 = 0\<close>
using div_mult_mod_eq [of a 1] by simp
-lemma bits_mod_0 [simp]:
+lemma bits_0_mod [simp]:
\<open>0 mod a = 0\<close>
using div_mult_mod_eq [of 0 a] by simp
-lemma mod_exp_div_exp_eq_0 [simp]:
- \<open>a mod 2 ^ n div 2 ^ n = 0\<close>
-proof (induction n arbitrary: a)
- case 0
- then show ?case
- by simp
-next
- case (Suc n)
- then have \<open>a div 2 ^ 1 mod 2 ^ n div 2 ^ n = 0\<close> .
- then show ?case
- using div_exp_eq [of _ 1 n] div_exp_mod_exp_eq [of a 1 n]
+lemma div_exp_eq_funpow_half:
+ \<open>a div 2 ^ n = ((\<lambda>a. a div 2) ^^ n) a\<close>
+proof -
+ have \<open>((\<lambda>a. a div 2) ^^ n) = (\<lambda>a. a div 2 ^ n)\<close>
+ by (induction n)
+ (simp_all del: funpow.simps power.simps add: power_0 funpow_Suc_right half_div_exp_eq)
+ then show ?thesis
by simp
qed
+lemma div_exp_eq:
+ \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
+ by (simp add: div_exp_eq_funpow_half Groups.add.commute [of m] funpow_add)
+
lemma bit_0:
\<open>bit a 0 \<longleftrightarrow> odd a\<close>
by (simp add: bit_iff_odd)
@@ -105,10 +74,6 @@
\<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
by (cases n) (simp_all add: bit_Suc bit_0)
-lemma bit_0_eq [simp]:
- \<open>bit 0 = \<bottom>\<close>
- by (simp add: fun_eq_iff bit_iff_odd)
-
context
fixes a
assumes stable: \<open>a div 2 = a\<close>
@@ -156,9 +121,35 @@
using \<open>a div 2 = a\<close> by (simp add: hyp)
qed
-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_iff_odd)
+lemma even_succ_div_exp [simp]:
+ \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close>
+proof (cases n)
+ case 0
+ with that show ?thesis
+ by simp
+next
+ case (Suc n)
+ with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close>
+ proof (induction n)
+ case 0
+ then show ?case
+ by simp
+ next
+ case (Suc n)
+ then show ?case
+ using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric]
+ by simp
+ qed
+ with Suc show ?thesis
+ by simp
+qed
+
+lemma even_succ_mod_exp [simp]:
+ \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
+ using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
+ by simp (metis (full_types) add.left_commute add_left_imp_eq)
+
+named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
where \<open>possible_bit TYPE('a) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
@@ -174,7 +165,7 @@
lemma bit_imp_possible_bit:
\<open>possible_bit TYPE('a) n\<close> if \<open>bit a n\<close>
- using that by (auto simp add: possible_bit_def exp_eq_0_imp_not_bit)
+ by (rule ccontr) (use that in \<open>auto simp add: bit_iff_odd possible_bit_def\<close>)
lemma impossible_bit:
\<open>\<not> bit a n\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
@@ -193,14 +184,14 @@
\<open>a = b\<close> if \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
proof -
have \<open>bit a n \<longleftrightarrow> bit b n\<close> for n
- proof (cases \<open>2 ^ n = 0\<close>)
+ proof (cases \<open>possible_bit TYPE('a) n\<close>)
+ case False
+ then show ?thesis
+ by (simp add: impossible_bit)
+ next
case True
then show ?thesis
- by (simp add: exp_eq_0_imp_not_bit)
- next
- case False
- then show ?thesis
- by (rule that[unfolded possible_bit_def])
+ by (rule that)
qed
then show ?thesis proof (induction a arbitrary: b rule: bit_induct)
case (stable a)
@@ -243,43 +234,6 @@
qed
qed
-lemma bit_eq_iff:
- \<open>a = b \<longleftrightarrow> (\<forall>n. possible_bit TYPE('a) n \<longrightarrow> bit a n \<longleftrightarrow> bit b n)\<close>
- by (auto intro: bit_eqI)
-
-named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
-
-lemma bit_exp_iff [bit_simps]:
- \<open>bit (2 ^ m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> m = n\<close>
- by (auto simp add: bit_iff_odd exp_div_exp_eq possible_bit_def)
-
-lemma bit_1_iff [bit_simps]:
- \<open>bit 1 n \<longleftrightarrow> n = 0\<close>
- using bit_exp_iff [of 0 n]
- by auto
-
-lemma bit_2_iff [bit_simps]:
- \<open>bit 2 n \<longleftrightarrow> possible_bit TYPE('a) 1 \<and> n = 1\<close>
- using bit_exp_iff [of 1 n] by auto
-
-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_iff_odd)
-
-lemma bit_double_iff [bit_simps]:
- \<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> possible_bit TYPE('a) n\<close>
- using even_mult_exp_div_exp_iff [of a 1 n]
- by (cases n, auto simp add: bit_iff_odd ac_simps possible_bit_def)
-
-lemma odd_bit_iff_bit_pred:
- \<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close>
-proof -
- from \<open>odd a\<close> obtain b where \<open>a = 2 * b + 1\<close> ..
- moreover have \<open>bit (2 * b) n \<or> n = 0 \<longleftrightarrow> bit (1 + 2 * b) n\<close>
- using even_bit_succ_iff by simp
- ultimately show ?thesis by (simp add: ac_simps)
-qed
-
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>)
proof
@@ -308,37 +262,97 @@
qed
qed
+lemma bit_eq_iff:
+ \<open>a = b \<longleftrightarrow> (\<forall>n. possible_bit TYPE('a) n \<longrightarrow> bit a n \<longleftrightarrow> bit b n)\<close>
+ by (auto intro: bit_eqI simp add: possible_bit_def)
+
+lemma bit_0_eq [simp]:
+ \<open>bit 0 = \<bottom>\<close>
+proof -
+ have \<open>0 div 2 ^ n = 0\<close> for n
+ unfolding div_exp_eq_funpow_half by (induction n) simp_all
+ then show ?thesis
+ by (simp add: fun_eq_iff bit_iff_odd)
+qed
+
+lemma bit_double_Suc_iff:
+ \<open>bit (2 * a) (Suc n) \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> bit a n\<close>
+ using even_double_div_exp_iff [of n a]
+ by (cases \<open>possible_bit TYPE('a) (Suc n)\<close>)
+ (auto simp add: bit_iff_odd possible_bit_def)
+
+lemma bit_double_iff [bit_simps]:
+ \<open>bit (2 * a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> 0 \<and> bit a (n - 1)\<close>
+ by (cases n) (simp_all add: bit_0 bit_double_Suc_iff)
+
+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_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>
+proof -
+ from \<open>odd a\<close> obtain b where \<open>a = 2 * b + 1\<close> ..
+ moreover have \<open>bit (2 * b) n \<or> n = 0 \<longleftrightarrow> bit (1 + 2 * b) n\<close>
+ using even_bit_succ_iff by simp
+ ultimately show ?thesis by (simp add: ac_simps)
+qed
+
+lemma bit_exp_iff [bit_simps]:
+ \<open>bit (2 ^ m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n = m\<close>
+proof (cases \<open>possible_bit TYPE('a) n\<close>)
+ case False
+ then show ?thesis
+ by (simp add: impossible_bit)
+next
+ case True
+ then show ?thesis
+ proof (induction n arbitrary: m)
+ case 0
+ show ?case
+ by (simp add: bit_0)
+ next
+ case (Suc n)
+ then have \<open>possible_bit TYPE('a) n\<close>
+ by (simp add: possible_bit_less_imp)
+ show ?case
+ proof (cases m)
+ case 0
+ then show ?thesis
+ by (simp add: bit_Suc)
+ next
+ case (Suc m)
+ with Suc.IH [of m] \<open>possible_bit TYPE('a) n\<close> show ?thesis
+ by (simp add: bit_double_Suc_iff)
+ qed
+ qed
+qed
+
+lemma bit_1_iff [bit_simps]:
+ \<open>bit 1 n \<longleftrightarrow> n = 0\<close>
+ using bit_exp_iff [of 0 n] by auto
+
+lemma bit_2_iff [bit_simps]:
+ \<open>bit 2 n \<longleftrightarrow> possible_bit TYPE('a) 1 \<and> n = 1\<close>
+ using bit_exp_iff [of 1 n] by auto
+
+lemma bit_of_bool_iff [bit_simps]:
+ \<open>bit (of_bool b) n \<longleftrightarrow> n = 0 \<and> b\<close>
+ by (simp add: bit_1_iff)
+
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_iff_odd)
-
-lemma bit_mask_sub_iff:
- \<open>bit (2 ^ m - 1) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < m\<close>
- by (simp add: bit_iff_odd even_mask_div_iff not_le possible_bit_def)
-
-lemma exp_add_not_zero_imp:
- \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
-proof -
- have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
- proof (rule notI)
- assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
- then have \<open>2 ^ (m + n) = 0\<close>
- by (rule disjE) (simp_all add: power_add)
- with that show False ..
- qed
- then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
- by simp_all
-qed
+ by (simp add: mod_2_eq_odd bit_simps)
lemma bit_disjunctive_add_iff:
\<open>bit (a + b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
-proof (cases \<open>2 ^ n = 0\<close>)
- case True
+proof (cases \<open>possible_bit TYPE('a) n\<close>)
+ case False
then show ?thesis
- by (simp add: exp_eq_0_imp_not_bit)
+ by (auto dest: impossible_bit)
next
- case False
+ case True
with that show ?thesis proof (induction n arbitrary: a b)
case 0
from "0.prems"(1) [of 0] show ?case
@@ -349,56 +363,21 @@
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(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
- from Suc.prems(2) have \<open>2 * 2 ^ n \<noteq> 0\<close> \<open>2 ^ n \<noteq> 0\<close>
- by (auto simp add: mult_2)
+ from Suc.prems(2) have \<open>possible_bit TYPE('a) (Suc n)\<close> \<open>possible_bit TYPE('a) n\<close>
+ by (simp_all add: possible_bit_less_imp)
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>2 * 2 ^ n \<noteq> 0\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
+ 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) n \<or> bit (b div 2) n\<close>
- using bit \<open>2 ^ n \<noteq> 0\<close> by (rule Suc.IH)
+ using bit \<open>possible_bit TYPE('a) n\<close> by (rule Suc.IH)
finally show ?case
by (simp add: bit_Suc)
qed
qed
-lemma
- exp_add_not_zero_imp_left: \<open>2 ^ m \<noteq> 0\<close>
- and exp_add_not_zero_imp_right: \<open>2 ^ n \<noteq> 0\<close>
- if \<open>2 ^ (m + n) \<noteq> 0\<close>
-proof -
- have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
- proof (rule notI)
- assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
- then have \<open>2 ^ (m + n) = 0\<close>
- by (rule disjE) (simp_all add: power_add)
- with that show False ..
- qed
- then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
- by simp_all
-qed
-
-lemma exp_not_zero_imp_exp_diff_not_zero:
- \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
-proof (cases \<open>m \<le> n\<close>)
- case True
- moreover define q where \<open>q = n - m\<close>
- ultimately have \<open>n = m + q\<close>
- by simp
- with that show ?thesis
- by (simp add: exp_add_not_zero_imp_right)
-next
- case False
- with that show ?thesis
- by simp
-qed
-
-lemma bit_of_bool_iff [bit_simps]:
- \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
- by (simp add: bit_1_iff)
-
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -454,25 +433,27 @@
with rec [of n True] show ?case
by simp
qed
- show \<open>q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\<close>
- for q m n :: nat
- apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin)
- apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes)
- done
- show \<open>(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\<close> if \<open>m \<le> n\<close>
- for q m n :: nat
- using that
- apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
- done
- show \<open>even ((2 ^ m - (1::nat)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::nat) \<or> m \<le> n\<close>
- for m n :: nat
- using even_mask_div_iff' [where ?'a = nat, of m n] by simp
- show \<open>even (q * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::nat) ^ n = 0 \<or> m \<le> n \<and> even (q div 2 ^ (n - m))\<close>
- for m n q r :: nat
- 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 bit_nat_def)
+ show \<open>even (((2 :: nat) ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> for m n :: nat
+ using even_decr_exp_div_exp_iff' [of m n] .
+ 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
@@ -497,12 +478,12 @@
lemma bit_of_nat_iff [bit_simps]:
\<open>bit (of_nat m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit m n\<close>
-proof (cases \<open>(2::'a) ^ n = 0\<close>)
- case True
+proof (cases \<open>possible_bit TYPE('a) n\<close>)
+ case False
then show ?thesis
- by (simp add: exp_eq_0_imp_not_bit possible_bit_def)
+ by (simp add: impossible_bit)
next
- case False
+ case True
then have \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
proof (induction m arbitrary: n rule: nat_bit_induct)
case zero
@@ -520,8 +501,8 @@
(auto simp add: bit_double_iff even_bit_succ_iff possible_bit_def
Bit_Operations.bit_Suc Bit_Operations.bit_0 dest: mult_not_zero)
qed
- with False show ?thesis
- by (simp add: possible_bit_def)
+ with True show ?thesis
+ by simp
qed
end
@@ -611,46 +592,27 @@
with rec [of k True] show ?case
by (simp add: ac_simps)
qed
- show \<open>(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
- for m n :: nat
- proof (cases \<open>m < n\<close>)
+ show \<open>even (((2 :: int) ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> for m n :: nat
+ using even_decr_exp_div_exp_iff' [of m n] .
+ 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
- then have \<open>n = m + (n - m)\<close>
+ moreover define r where \<open>r = n - m\<close>
+ ultimately have \<open>n = m + r\<close>
by simp
- then have \<open>(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))\<close>
- by simp
- also have \<open>\<dots> = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))\<close>
- by (simp add: power_add)
- also have \<open>\<dots> = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)\<close>
- by (simp add: zdiv_zmult2_eq)
- finally show ?thesis using \<open>m < n\<close> by simp
+ with True show ?thesis
+ by (simp add: power_add zdiv_zmult2_eq)
next
case False
- then show ?thesis
- by (simp add: power_diff)
+ 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
- show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close>
- for m n :: nat and k :: int
- using mod_exp_eq [of \<open>nat k\<close> m n]
- apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
- apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add)
- apply (simp only: flip: mult.left_commute [of \<open>2 ^ m\<close>])
- apply (subst zmod_zmult2_eq) apply simp_all
- done
- show \<open>(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\<close>
- if \<open>m \<le> n\<close> for m n :: nat and k :: int
- using that
- apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
- done
- show \<open>even ((2 ^ m - (1::int)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::int) \<or> m \<le> n\<close>
- for m n :: nat
- using even_mask_div_iff' [where ?'a = int, of m n] by simp
- show \<open>even (k * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::int) ^ n = 0 \<or> m \<le> n \<and> even (k div 2 ^ (n - m))\<close>
- for m n :: nat and k l :: int
- 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 bit_int_def)
+qed (auto simp add: zdiv_zmult2_eq bit_int_def)
end
@@ -715,6 +677,14 @@
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_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>
+ by (simp add: bit_iff_odd_drop_bit)
+
lemma bit_and_iff [bit_simps]:
\<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
proof (induction n arbitrary: a b)
@@ -816,13 +786,71 @@
\<open>a XOR a = 0\<close>
by (rule bit_eqI) (simp add: bit_simps)
-lemma bit_iff_odd_drop_bit:
- \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
- 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>
- by (simp add: bit_iff_odd_drop_bit)
+lemma bit_mask_iff [bit_simps]:
+ \<open>bit (mask m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < m\<close>
+ apply (cases \<open>possible_bit TYPE('a) n\<close>)
+ apply (simp add: bit_iff_odd mask_eq_exp_minus_1 possible_bit_def even_decr_exp_div_exp_iff not_le)
+ apply (simp add: impossible_bit)
+ done
+
+lemma even_mask_iff:
+ \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
+ using bit_mask_iff [of n 0] by (auto simp add: bit_0)
+
+lemma mask_0 [simp]:
+ \<open>mask 0 = 0\<close>
+ by (simp add: mask_eq_exp_minus_1)
+
+lemma mask_Suc_0 [simp]:
+ \<open>mask (Suc 0) = 1\<close>
+ by (simp add: mask_eq_exp_minus_1 add_implies_diff sym)
+
+lemma mask_Suc_exp:
+ \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
+ by (auto simp add: bit_eq_iff bit_simps)
+
+lemma mask_Suc_double:
+ \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
+ by (auto simp add: bit_eq_iff bit_simps elim: possible_bit_less_imp)
+
+lemma mask_numeral:
+ \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
+ by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)
+
+lemma push_bit_0_id [simp]:
+ \<open>push_bit 0 = id\<close>
+ by (simp add: fun_eq_iff push_bit_eq_mult)
+
+lemma push_bit_Suc [simp]:
+ \<open>push_bit (Suc n) a = push_bit n (a * 2)\<close>
+ by (simp add: push_bit_eq_mult ac_simps)
+
+lemma push_bit_double:
+ \<open>push_bit n (a * 2) = push_bit n a * 2\<close>
+ by (simp add: push_bit_eq_mult ac_simps)
+
+lemma bit_push_bit_iff [bit_simps]:
+ \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m)\<close>
+proof (induction n arbitrary: m)
+ case 0
+ then show ?case
+ by (auto simp add: bit_0 push_bit_eq_mult)
+next
+ case (Suc n)
+ show ?case
+ proof (cases m)
+ case 0
+ then show ?thesis
+ by (auto simp add: bit_imp_possible_bit)
+ next
+ case (Suc m)
+ with Suc.prems Suc.IH [of m] show ?thesis
+ apply (simp add: push_bit_double)
+ apply (simp add: bit_simps mult.commute [of _ 2])
+ apply (auto simp add: possible_bit_less_imp)
+ done
+ qed
+qed
lemma div_push_bit_of_1_eq_drop_bit:
\<open>a div push_bit n 1 = drop_bit n a\<close>
@@ -836,10 +864,6 @@
\<open>push_bit m (push_bit n a) = push_bit (m + n) a\<close>
by (simp add: push_bit_eq_mult power_add ac_simps)
-lemma push_bit_0_id [simp]:
- \<open>push_bit 0 = id\<close>
- by (simp add: fun_eq_iff push_bit_eq_mult)
-
lemma push_bit_of_0 [simp]:
\<open>push_bit n 0 = 0\<close>
by (simp add: push_bit_eq_mult)
@@ -848,14 +872,6 @@
\<open>push_bit n 1 = 2 ^ n\<close>
by (simp add: push_bit_eq_mult)
-lemma push_bit_Suc [simp]:
- \<open>push_bit (Suc n) a = push_bit n (a * 2)\<close>
- by (simp add: push_bit_eq_mult ac_simps)
-
-lemma push_bit_double:
- \<open>push_bit n (a * 2) = push_bit n a * 2\<close>
- by (simp add: push_bit_eq_mult ac_simps)
-
lemma push_bit_add:
\<open>push_bit n (a + b) = push_bit n a + push_bit n b\<close>
by (simp add: push_bit_eq_mult algebra_simps)
@@ -868,15 +884,20 @@
"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_diff_exp_iff not_le)
+
lemma take_bit_Suc:
- \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close>
-proof -
- have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
- using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>]
- mult_exp_mod_exp_eq [of 1 \<open>Suc n\<close> \<open>a div 2\<close>]
- by (auto simp add: take_bit_eq_mod ac_simps)
- then show ?thesis
- using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
+ \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
+proof (rule bit_eqI)
+ fix m
+ assume \<open>possible_bit TYPE('a) m\<close>
+ then show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
+ apply (cases a rule: parity_cases; cases m)
+ apply (simp_all add: bit_simps even_bit_succ_iff mult.commute [of _ 2] add.commute [of _ 1] flip: bit_Suc)
+ apply (simp_all add: bit_0)
+ done
qed
lemma take_bit_rec:
@@ -889,19 +910,23 @@
lemma take_bit_of_0 [simp]:
\<open>take_bit n 0 = 0\<close>
- by (simp add: take_bit_eq_mod)
+ by (rule bit_eqI) (simp add: bit_simps)
lemma take_bit_of_1 [simp]:
\<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 (simp add: drop_bit_eq_div)
+ by (rule bit_eqI) (simp add: bit_simps)
lemma drop_bit_of_1 [simp]:
\<open>drop_bit n 1 = of_bool (n = 0)\<close>
- by (simp add: drop_bit_eq_div)
+ by (rule bit_eqI) (simp add: bit_simps ac_simps)
lemma drop_bit_0 [simp]:
\<open>drop_bit 0 = id\<close>
@@ -929,7 +954,7 @@
lemma take_bit_take_bit [simp]:
\<open>take_bit m (take_bit n a) = take_bit (min m n) a\<close>
- by (simp add: take_bit_eq_mod mod_exp_eq ac_simps)
+ by (rule bit_eqI) (simp add: bit_simps)
lemma drop_bit_drop_bit [simp]:
\<open>drop_bit m (drop_bit n a) = drop_bit (m + n) a\<close>
@@ -937,79 +962,33 @@
lemma push_bit_take_bit:
\<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
- apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps)
- using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add)
- done
+ by (rule bit_eqI) (auto simp add: bit_simps)
lemma take_bit_push_bit:
\<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
-proof (cases \<open>m \<le> n\<close>)
- case True
- then show ?thesis
- apply (simp add:)
- apply (simp_all add: push_bit_eq_mult take_bit_eq_mod)
- apply (auto dest!: le_Suc_ex simp add: power_add ac_simps)
- using mult_exp_mod_exp_eq [of m m \<open>a * 2 ^ n\<close> for n]
- apply (simp add: ac_simps)
- done
-next
- case False
- then show ?thesis
- using push_bit_take_bit [of n \<open>m - n\<close> a]
- by simp
-qed
+ by (rule bit_eqI) (auto simp add: bit_simps)
lemma take_bit_drop_bit:
\<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
- by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq)
+ by (rule bit_eqI) (auto simp add: bit_simps)
lemma drop_bit_take_bit:
\<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
-proof (cases "m \<le> n")
- case True
- then show ?thesis
- using take_bit_drop_bit [of "n - m" m a] by simp
-next
- case False
- then obtain q where \<open>m = n + q\<close>
- by (auto simp add: not_le dest: less_imp_Suc_add)
- then have \<open>drop_bit m (take_bit n a) = 0\<close>
- using div_exp_eq [of \<open>a mod 2 ^ n\<close> n q]
- by (simp add: take_bit_eq_mod drop_bit_eq_div)
- with False show ?thesis
- by simp
-qed
+ by (rule bit_eqI) (auto simp add: bit_simps)
lemma even_push_bit_iff [simp]:
\<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
by (simp add: push_bit_eq_mult) auto
-lemma bit_push_bit_iff [bit_simps]:
- \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m)\<close>
- by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff possible_bit_def)
-
-lemma bit_drop_bit_eq [bit_simps]:
- \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
- by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
-
-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: 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>
if \<open>a div 2 = a\<close>
by (induction n) (simp_all add: that drop_bit_Suc)
lemma stable_imp_take_bit_eq:
- \<open>take_bit n a = (if even a then 0 else 2 ^ n - 1)\<close>
+ \<open>take_bit n a = (if even a then 0 else mask n)\<close>
if \<open>a div 2 = a\<close>
-proof (rule bit_eqI[unfolded possible_bit_def])
- fix m
- assume \<open>2 ^ m \<noteq> 0\<close>
- with that show \<open>bit (take_bit n a) m \<longleftrightarrow> bit (if even a then 0 else 2 ^ n - 1) m\<close>
- by (simp add: bit_take_bit_iff bit_mask_sub_iff possible_bit_def stable_imp_bit_iff_odd)
-qed
+ by (rule bit_eqI) (use that in \<open>simp add: bit_simps stable_imp_bit_iff_odd\<close>)
lemma exp_dvdE:
assumes \<open>2 ^ n dvd a\<close>
@@ -1114,34 +1093,6 @@
\<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
by (auto simp add: bit_eq_iff bit_simps)
-lemma bit_mask_iff [bit_simps]:
- \<open>bit (mask m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < m\<close>
- by (simp add: mask_eq_exp_minus_1 bit_mask_sub_iff)
-
-lemma even_mask_iff:
- \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
- using bit_mask_iff [of n 0] by (auto simp add: bit_0)
-
-lemma mask_0 [simp]:
- \<open>mask 0 = 0\<close>
- by (simp add: mask_eq_exp_minus_1)
-
-lemma mask_Suc_0 [simp]:
- \<open>mask (Suc 0) = 1\<close>
- by (simp add: mask_eq_exp_minus_1 add_implies_diff sym)
-
-lemma mask_Suc_exp:
- \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
- by (auto simp add: bit_eq_iff bit_simps)
-
-lemma mask_Suc_double:
- \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
- by (auto simp add: bit_eq_iff bit_simps elim: possible_bit_less_imp)
-
-lemma mask_numeral:
- \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
- by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)
-
lemma take_bit_of_mask [simp]:
\<open>take_bit m (mask n) = mask (min m n)\<close>
by (rule bit_eqI) (simp add: bit_simps)
@@ -1164,10 +1115,7 @@
lemma bit_iff_and_push_bit_not_eq_0:
\<open>bit a n \<longleftrightarrow> a AND push_bit n 1 \<noteq> 0\<close>
- apply (cases \<open>2 ^ n = 0\<close>)
- apply (simp_all add: bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit)
- apply (simp_all add: bit_exp_iff)
- done
+ by (cases \<open>possible_bit TYPE('a) n\<close>) (simp_all add: bit_eq_iff bit_simps impossible_bit)
lemma bit_set_bit_iff [bit_simps]:
\<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
@@ -1449,10 +1397,7 @@
lemma take_bit_not_iff:
\<open>take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b\<close>
- apply (simp add: bit_eq_iff)
- apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
- apply (use exp_eq_0_imp_not_bit in blast)
- done
+ by (auto simp add: bit_eq_iff bit_simps)
lemma take_bit_not_eq_mask_diff:
\<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
@@ -1513,12 +1458,7 @@
lemma push_bit_mask_eq:
\<open>push_bit m (mask n) = mask (n + m) AND NOT (mask m)\<close>
- apply (rule bit_eqI)
- apply (auto simp add: bit_simps not_less possible_bit_def)
- apply (drule sym [of 0])
- apply (simp only:)
- using exp_not_zero_imp_exp_diff_not_zero apply (blast dest: exp_not_zero_imp_exp_diff_not_zero)
- done
+ by (rule bit_eqI) (auto simp add: bit_simps not_less possible_bit_less_imp)
lemma slice_eq_mask:
\<open>push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)\<close>
@@ -3755,9 +3695,105 @@
subsection \<open>Lemma duplicates and other\<close>
+context semiring_bits
+begin
+
+lemma even_mask_div_iff [no_atp]:
+ \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
+ by (cases \<open>2 ^ n = 0\<close>) (simp_all add: even_decr_exp_div_exp_iff)
+
+lemma exp_div_exp_eq [no_atp]:
+ \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
+ apply (rule bit_eqI)
+ using bit_exp_iff div_exp_eq apply (auto simp add: bit_iff_odd possible_bit_def)
+ done
+
+lemma bits_1_div_2 [no_atp]:
+ \<open>1 div 2 = 0\<close>
+ by (fact half_1)
+
+lemma bits_1_div_exp [no_atp]:
+ \<open>1 div 2 ^ n = of_bool (n = 0)\<close>
+ using div_exp_eq [of 1 1] by (cases n) simp_all
+
+lemmas bits_div_0 = bits_0_div
+
+lemmas bits_mod_0 = bits_0_mod
+
+lemma exp_add_not_zero_imp [no_atp]:
+ \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+ have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+ proof (rule notI)
+ assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+ then have \<open>2 ^ (m + n) = 0\<close>
+ by (rule disjE) (simp_all add: power_add)
+ with that show False ..
+ qed
+ then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+ by simp_all
+qed
+
+lemma
+ exp_add_not_zero_imp_left [no_atp]: \<open>2 ^ m \<noteq> 0\<close>
+ and exp_add_not_zero_imp_right [no_atp]: \<open>2 ^ n \<noteq> 0\<close>
+ if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+ have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+ proof (rule notI)
+ assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+ then have \<open>2 ^ (m + n) = 0\<close>
+ by (rule disjE) (simp_all add: power_add)
+ with that show False ..
+ qed
+ then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+ by simp_all
+qed
+
+lemma exp_not_zero_imp_exp_diff_not_zero [no_atp]:
+ \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
+proof (cases \<open>m \<le> n\<close>)
+ case True
+ moreover define q where \<open>q = n - m\<close>
+ ultimately have \<open>n = m + q\<close>
+ by simp
+ with that show ?thesis
+ by (simp add: exp_add_not_zero_imp_right)
+next
+ case False
+ with that show ?thesis
+ by simp
+qed
+
+lemma exp_eq_0_imp_not_bit [no_atp]:
+ \<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
+ using that by (simp add: bit_iff_odd)
+
+end
+
context semiring_bit_operations
begin
+lemma mod_exp_eq [no_atp]:
+ \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
+ by (simp flip: take_bit_eq_mod add: ac_simps)
+
+lemma mult_exp_mod_exp_eq [no_atp]:
+ \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
+ by (simp flip: push_bit_eq_mult take_bit_eq_mod add: push_bit_take_bit)
+
+lemma div_exp_mod_exp_eq [no_atp]:
+ \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
+ by (simp flip: drop_bit_eq_div take_bit_eq_mod add: drop_bit_take_bit)
+
+lemma even_mult_exp_div_exp_iff [no_atp]:
+ \<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>
+ by (simp flip: push_bit_eq_mult drop_bit_eq_div add: even_drop_bit_iff_not_bit bit_simps possible_bit_def) auto
+
+lemma mod_exp_div_exp_eq_0 [no_atp]:
+ \<open>a mod 2 ^ n div 2 ^ n = 0\<close>
+ by (simp flip: take_bit_eq_mod drop_bit_eq_div add: drop_bit_take_bit)
+
lemmas bits_one_mod_two_eq_one [no_atp] = one_mod_two_eq_one
lemmas set_bit_def [no_atp] = set_bit_eq_or
--- a/src/HOL/Code_Numeral.thy Fri Jan 26 11:19:22 2024 +0000
+++ b/src/HOL/Code_Numeral.thy Fri Jan 26 11:19:30 2024 +0000
@@ -348,15 +348,16 @@
is take_bit .
instance by (standard; transfer)
- (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
- bits_div_0 bits_div_by_0 bits_div_by_1 even_half_succ_eq
- 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
+ (fact bit_induct bits_div_by_0 bits_div_by_1 bits_0_div even_half_succ_eq
+ half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_diff_exp_iff
+ 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)+
end
+
+
instance integer :: linordered_euclidean_semiring_bit_operations ..
context
@@ -1107,11 +1108,11 @@
is take_bit .
instance by (standard; transfer)
- (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
- bits_div_0 bits_div_by_0 bits_div_by_1 even_half_succ_eq
- 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 and_rec or_rec xor_rec
- mask_eq_exp_minus_1 set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor)+
+ (fact bit_induct bits_div_by_0 bits_div_by_1 bits_0_div even_half_succ_eq
+ half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_diff_exp_iff
+ 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)+
end
--- a/src/HOL/Library/Word.thy Fri Jan 26 11:19:22 2024 +0000
+++ b/src/HOL/Library/Word.thy Fri Jan 26 11:19:30 2024 +0000
@@ -828,56 +828,39 @@
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
show \<open>a div 0 = 0\<close>
for a :: \<open>'a word\<close>
by transfer simp
show \<open>a div 1 = a\<close>
for a :: \<open>'a word\<close>
by transfer simp
+ show \<open>0 div a = 0\<close>
+ for a :: \<open>'a word\<close>
+ by transfer simp
show \<open>(1 + a) div 2 = a div 2\<close>
if \<open>even a\<close>
for a :: \<open>'a word\<close>
using that by transfer
(auto dest: le_Suc_ex simp add: take_bit_Suc elim!: evenE)
- show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
- for m n :: nat
- by transfer (simp, simp add: exp_div_exp_eq)
- show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
- for a :: "'a word" and m n :: nat
+ 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
- apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div)
+ using drop_bit_eq_div [symmetric, where ?'a = int,of _ 1]
+ apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div simp del: power.simps)
apply (simp add: drop_bit_take_bit)
done
- show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
- for a :: "'a word" and m n :: nat
- by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps)
- show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
- if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat
- using that apply transfer
- apply (auto simp flip: take_bit_eq_mod)
- apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin)
- done
- show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
- for a :: "'a word" and m n :: nat
- by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
- show \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close>
+ show \<open>even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close> if \<open>2 ^ Suc n \<noteq> (0::'a word)\<close>
+ 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 ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> m \<le> n\<close> if \<open>2 ^ n \<noteq> (0::'a word)\<close>
for m n :: nat
- by transfer
+ using that by transfer
(simp flip: drop_bit_eq_div mask_eq_exp_minus_1 add: bit_simps even_drop_bit_iff_not_bit not_less)
- show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n - m))\<close>
+ 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
- proof transfer
- show \<open>even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \<longleftrightarrow>
- n < m
- \<or> take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0
- \<or> (m \<le> n \<and> even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\<close>
- for m n :: nat and k l :: int
- by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult
- simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m])
- qed
+ 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
--- a/src/HOL/Parity.thy Fri Jan 26 11:19:22 2024 +0000
+++ b/src/HOL/Parity.thy Fri Jan 26 11:19:30 2024 +0000
@@ -925,7 +925,7 @@
context linordered_euclidean_semiring
begin
-lemma even_mask_div_iff':
+lemma even_decr_exp_div_exp_iff':
\<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
proof -
have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close>