--- a/src/HOL/Parity.thy Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/Parity.thy Fri May 08 06:26:28 2020 +0000
@@ -934,6 +934,10 @@
qed
qed
+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)
+
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)
@@ -1204,7 +1208,7 @@
by (simp add: take_bit_eq_mod)
lemma take_bit_Suc:
- \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
+ \<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>]
@@ -1215,7 +1219,7 @@
qed
lemma take_bit_rec:
- \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + of_bool (odd a))\<close>
+ \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + a mod 2)\<close>
by (cases n) (simp_all add: take_bit_Suc)
lemma take_bit_Suc_0 [simp]:
@@ -1442,7 +1446,7 @@
lemma take_bit_Suc_bit1 [simp]:
\<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
- by (simp add: take_bit_Suc numeral_Bit1_div_2)
+ by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
lemma take_bit_numeral_bit0 [simp]:
\<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
@@ -1450,7 +1454,7 @@
lemma take_bit_numeral_bit1 [simp]:
\<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
- by (simp add: take_bit_rec numeral_Bit1_div_2)
+ by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
lemma take_bit_of_nat:
"take_bit n (of_nat m) = of_nat (take_bit n m)"
--- a/src/HOL/Set_Interval.thy Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/Set_Interval.thy Fri May 08 06:26:28 2020 +0000
@@ -2087,7 +2087,7 @@
= (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
finally show ?case
- using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc)
+ using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc mod_2_eq_odd)
qed
end
--- a/src/HOL/String.thy Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/String.thy Fri May 08 06:26:28 2020 +0000
@@ -90,7 +90,7 @@
also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
finally show ?thesis
- using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps)
+ using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps mod_2_eq_odd)
qed
qed
--- a/src/HOL/ex/Bit_Operations.thy Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy Fri May 08 06:26:28 2020 +0000
@@ -46,26 +46,26 @@
by (simp add: bit_eq_iff bit_and_iff)
lemma one_and_eq [simp]:
- "1 AND a = of_bool (odd a)"
+ "1 AND a = a mod 2"
by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
lemma and_one_eq [simp]:
- "a AND 1 = of_bool (odd a)"
+ "a AND 1 = a mod 2"
using one_and_eq [of a] by (simp add: ac_simps)
-lemma one_or_eq [simp]:
+lemma one_or_eq:
"1 OR a = a + of_bool (even a)"
by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)
-lemma or_one_eq [simp]:
+lemma or_one_eq:
"a OR 1 = a + of_bool (even a)"
using one_or_eq [of a] by (simp add: ac_simps)
-lemma one_xor_eq [simp]:
+lemma one_xor_eq:
"1 XOR a = a + of_bool (even a) - of_bool (odd a)"
by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE)
-lemma xor_one_eq [simp]:
+lemma xor_one_eq:
"a XOR 1 = a + of_bool (even a) - of_bool (odd a)"
using one_xor_eq [of a] by (simp add: ac_simps)
@@ -533,26 +533,26 @@
by (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
lemma Suc_0_and_eq [simp]:
- \<open>Suc 0 AND n = of_bool (odd n)\<close>
+ \<open>Suc 0 AND n = n mod 2\<close>
using one_and_eq [of n] by simp
lemma and_Suc_0_eq [simp]:
- \<open>n AND Suc 0 = of_bool (odd n)\<close>
+ \<open>n AND Suc 0 = n mod 2\<close>
using and_one_eq [of n] by simp
-lemma Suc_0_or_eq [simp]:
+lemma Suc_0_or_eq:
\<open>Suc 0 OR n = n + of_bool (even n)\<close>
using one_or_eq [of n] by simp
-lemma or_Suc_0_eq [simp]:
+lemma or_Suc_0_eq:
\<open>n OR Suc 0 = n + of_bool (even n)\<close>
using or_one_eq [of n] by simp
-lemma Suc_0_xor_eq [simp]:
+lemma Suc_0_xor_eq:
\<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
using one_xor_eq [of n] by simp
-lemma xor_Suc_0_eq [simp]:
+lemma xor_Suc_0_eq:
\<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
using xor_one_eq [of n] by simp
--- a/src/HOL/ex/Word.thy Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/ex/Word.thy Fri May 08 06:26:28 2020 +0000
@@ -592,7 +592,8 @@
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)
+ using that by transfer
+ (auto dest: le_Suc_ex simp add: mod_2_eq_odd 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)