--- a/src/HOL/Euclidean_Division.thy Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy Sat Feb 01 19:10:37 2020 +0100
@@ -1933,7 +1933,7 @@
by (simp add: of_nat_mod)
qed
-lemma range_mod_exp:
+lemma mask_mod_exp:
\<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close>
proof -
have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>)
--- a/src/HOL/Parity.thy Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/Parity.thy Sat Feb 01 19:10:37 2020 +0100
@@ -150,6 +150,19 @@
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
by (induct n) auto
+lemma mask_eq_sum_exp:
+ \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
+proof -
+ have *: \<open>{q. q < Suc m} = insert m {q. q < m}\<close> for m
+ by auto
+ have \<open>2 ^ n = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1\<close>
+ by (induction n) (simp_all add: ac_simps mult_2 *)
+ then have \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1 - 1\<close>
+ by simp
+ then show ?thesis
+ by simp
+qed
+
end
class ring_parity = ring + semiring_parity
@@ -398,6 +411,43 @@
qed
qed
+context semiring_parity
+begin
+
+lemma even_sum_iff:
+ \<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close>
+using that proof (induction A)
+ case empty
+ then show ?case
+ by simp
+next
+ case (insert a A)
+ moreover have \<open>{b \<in> insert a A. odd (f b)} = (if odd (f a) then {a} else {}) \<union> {b \<in> A. odd (f b)}\<close>
+ by auto
+ ultimately show ?case
+ by simp
+qed
+
+lemma even_prod_iff:
+ \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close>
+ using that by (induction A) simp_all
+
+lemma even_mask_iff [simp]:
+ \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
+proof (cases \<open>n = 0\<close>)
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ then have \<open>{a. a = 0 \<and> a < n} = {0}\<close>
+ by auto
+ then show ?thesis
+ by (auto simp add: mask_eq_sum_exp even_sum_iff)
+qed
+
+end
+
subsection \<open>Parity and powers\<close>
@@ -1162,6 +1212,38 @@
end
+lemma bit_push_bit_iff_nat:
+ \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
+proof (cases \<open>m \<le> n\<close>)
+ case True
+ then obtain r where \<open>n = m + r\<close>
+ using le_Suc_ex by blast
+ with True show ?thesis
+ by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
+next
+ case False
+ then obtain r where \<open>m = Suc (n + r)\<close>
+ using less_imp_Suc_add not_le by blast
+ with False show ?thesis
+ by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
+qed
+
+lemma bit_push_bit_iff_int:
+ \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
+proof (cases \<open>m \<le> n\<close>)
+ case True
+ then obtain r where \<open>n = m + r\<close>
+ using le_Suc_ex by blast
+ with True show ?thesis
+ by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
+next
+ case False
+ then obtain r where \<open>m = Suc (n + r)\<close>
+ using less_imp_Suc_add not_le by blast
+ with False show ?thesis
+ by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
+qed
+
class unique_euclidean_semiring_with_bit_shifts =
unique_euclidean_semiring_with_nat + semiring_bit_shifts
begin
@@ -1174,9 +1256,9 @@
\<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
using take_bit_of_exp [of n 1] by simp
-lemma take_bit_of_range:
+lemma take_bit_of_mask:
\<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
- by (simp add: take_bit_eq_mod range_mod_exp)
+ by (simp add: take_bit_eq_mod mask_mod_exp)
lemma push_bit_eq_0_iff [simp]:
"push_bit n a = 0 \<longleftrightarrow> a = 0"
@@ -1230,6 +1312,39 @@
"drop_bit n (of_nat m) = of_nat (drop_bit n m)"
by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+lemma bit_of_nat_iff_bit [simp]:
+ \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
+proof -
+ have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
+ by simp
+ 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)
+qed
+
+lemma of_nat_push_bit:
+ \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
+ by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma of_nat_drop_bit:
+ \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
+ by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
+
+lemma of_nat_take_bit:
+ \<open>of_nat (take_bit m n) = take_bit m (of_nat n)\<close>
+ by (simp add: take_bit_eq_mod semiring_bit_shifts_class.take_bit_eq_mod of_nat_mod)
+
+lemma bit_push_bit_iff_of_nat_iff:
+ \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+proof -
+ from bit_push_bit_iff_nat
+ have \<open>bit (of_nat (push_bit m r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+ by simp
+ then show ?thesis
+ by (simp add: of_nat_push_bit)
+qed
+
end
instance nat :: unique_euclidean_semiring_with_bit_shifts ..
--- a/src/HOL/ex/Bit_Operations.thy Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/ex/Bit_Operations.thy Sat Feb 01 19:10:37 2020 +0100
@@ -9,40 +9,16 @@
Main
begin
-lemma bit_push_bit_eq_int:
- \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
-proof (cases \<open>m \<le> n\<close>)
- case True
- then obtain q where \<open>n = m + q\<close>
- using le_Suc_ex by blast
- with True show ?thesis
- by (simp add: push_bit_eq_mult bit_def power_add)
-next
- case False
- then obtain q where \<open>m = Suc (n + q)\<close>
- using less_imp_Suc_add not_le by blast
- with False show ?thesis
- by (simp add: push_bit_eq_mult bit_def power_add)
-qed
-
context semiring_bits
begin
-(*lemma range_rec:
- \<open>2 ^ Suc n - 1 = 1 + 2 * (2 ^ n - 1)\<close>
+(*lemma even_mask_div_iff:
+ \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
sorry
-lemma even_range_div_iff:
- \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
- sorry*)
-
-(*lemma even_range_iff [simp]:
- \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
- by (induction n) (simp_all only: range_rec, simp_all)
-
-lemma bit_range_iff:
+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_range_div_iff not_le)*)
+ by (simp add: bit_def even_mask_div_iff not_le)*)
end
@@ -129,6 +105,30 @@
\<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
by (simp add: flip_bit_def)
+lemma zero_and_eq [simp]:
+ "0 AND a = 0"
+ by (simp add: bit_eq_iff bit_and_iff)
+
+lemma and_zero_eq [simp]:
+ "a AND 0 = 0"
+ by (simp add: bit_eq_iff bit_and_iff)
+
+lemma zero_or_eq [simp]:
+ "0 OR a = a"
+ by (simp add: bit_eq_iff bit_or_iff)
+
+lemma or_zero_eq [simp]:
+ "a OR 0 = a"
+ by (simp add: bit_eq_iff bit_or_iff)
+
+lemma zero_xor_eq [simp]:
+ "0 XOR a = a"
+ by (simp add: bit_eq_iff bit_xor_iff)
+
+lemma xor_zero_eq [simp]:
+ "a XOR 0 = a"
+ by (simp add: bit_eq_iff bit_xor_iff)
+
lemma take_bit_and [simp]:
\<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
@@ -209,6 +209,10 @@
done
qed
+lemma push_bit_minus:
+ \<open>push_bit n (- a) = - push_bit n a\<close>
+ by (simp add: push_bit_eq_mult)
+
lemma take_bit_not_take_bit:
\<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
@@ -327,14 +331,6 @@
declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
\<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-lemma zero_nat_and_eq [simp]:
- "0 AND n = 0" for n :: nat
- by simp
-
-lemma and_zero_nat_eq [simp]:
- "n AND 0 = 0" for n :: nat
- by simp
-
global_interpretation or_nat: zip_nat "(\<or>)"
defines or_nat = or_nat.F
by standard auto
@@ -348,14 +344,6 @@
declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
\<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-lemma zero_nat_or_eq [simp]:
- "0 OR n = n" for n :: nat
- by simp
-
-lemma or_zero_nat_eq [simp]:
- "n OR 0 = n" for n :: nat
- by simp
-
global_interpretation xor_nat: zip_nat "(\<noteq>)"
defines xor_nat = xor_nat.F
by standard auto
@@ -363,14 +351,6 @@
declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
\<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-lemma zero_nat_xor_eq [simp]:
- "0 XOR n = n" for n :: nat
- by simp
-
-lemma xor_zero_nat_eq [simp]:
- "n XOR 0 = n" for n :: nat
- by simp
-
instance proof
fix m n q :: nat
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
@@ -678,22 +658,6 @@
by (simp add: and_int.self)
qed
-lemma zero_int_and_eq [simp]:
- "0 AND k = 0" for k :: int
- by simp
-
-lemma and_zero_int_eq [simp]:
- "k AND 0 = 0" for k :: int
- by simp
-
-lemma minus_int_and_eq [simp]:
- "- 1 AND k = k" for k :: int
- by simp
-
-lemma and_minus_int_eq [simp]:
- "k AND - 1 = k" for k :: int
- by simp
-
global_interpretation or_int: zip_int "(\<or>)"
defines or_int = or_int.F
by standard
@@ -707,22 +671,6 @@
by (simp add: or_int.self)
qed
-lemma zero_int_or_eq [simp]:
- "0 OR k = k" for k :: int
- by simp
-
-lemma and_zero_or_eq [simp]:
- "k OR 0 = k" for k :: int
- by simp
-
-lemma minus_int_or_eq [simp]:
- "- 1 OR k = - 1" for k :: int
- by simp
-
-lemma or_minus_int_eq [simp]:
- "k OR - 1 = - 1" for k :: int
- by simp
-
global_interpretation xor_int: zip_int "(\<noteq>)"
defines xor_int = xor_int.F
by standard
@@ -730,42 +678,6 @@
declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
\<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-lemma zero_int_xor_eq [simp]:
- "0 XOR k = k" for k :: int
- by simp
-
-lemma and_zero_xor_eq [simp]:
- "k XOR 0 = k" for k :: int
- by simp
-
-lemma minus_int_xor_eq [simp]:
- "- 1 XOR k = complement k" for k :: int
- by simp
-
-lemma xor_minus_int_eq [simp]:
- "k XOR - 1 = complement k" for k :: int
- by simp
-
-lemma not_div_2:
- "NOT k div 2 = NOT (k div 2)"
- for k :: int
- by (simp add: complement_div_2 not_int_def)
-
-lemma not_int_simps [simp]:
- "NOT 0 = (- 1 :: int)"
- "NOT (- 1) = (0 :: int)"
- "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
- by (auto simp add: not_int_def elim: oddE)
-
-lemma not_one_int [simp]:
- "NOT 1 = (- 2 :: int)"
- by simp
-
-lemma even_not_iff [simp]:
- "even (NOT k) \<longleftrightarrow> odd k"
- for k :: int
- by (simp add: not_int_def)
-
lemma bit_not_iff_int:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int
@@ -810,12 +722,28 @@
end
+lemma not_div_2:
+ "NOT k div 2 = NOT (k div 2)" for k :: int
+ by (simp add: complement_div_2 not_int_def)
+
+lemma not_int_rec [simp]:
+ "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+ by (auto simp add: not_int_def elim: oddE)
+
+lemma not_one_int [simp]:
+ "NOT 1 = (- 2 :: int)"
+ by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
+
+lemma even_not_int_iff [simp]:
+ "even (NOT k) \<longleftrightarrow> odd k" for k :: int
+ using bit_not_iff [of k 0] by auto
+
lemma one_and_int_eq [simp]:
- "1 AND k = k mod 2" for k :: int
- by (simp add: bit_eq_iff bit_and_iff mod2_eq_if) (auto simp add: bit_1_iff)
+ "1 AND k = of_bool (odd k)" for k :: int
+ by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
lemma and_one_int_eq [simp]:
- "k AND 1 = k mod 2" for k :: int
+ "k AND 1 = of_bool (odd k)" for k :: int
using one_and_int_eq [of 1] by (simp add: ac_simps)
lemma one_or_int_eq [simp]:
--- a/src/HOL/ex/Word.thy Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/ex/Word.thy Sat Feb 01 19:10:37 2020 +0100
@@ -546,11 +546,11 @@
n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
by transfer
(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_eq_int)
+ simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
-(*lemma even_range_div_iff_word:
+(*lemma even_mask_div_iff_word:
\<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a::len word) \<or> m \<le> n\<close>
- by transfer (auto simp add: take_bit_of_range even_range_div_iff)*)
+ by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*)
instance word :: (len) semiring_bits
proof