--- a/src/HOL/Parity.thy Sat Apr 25 16:31:43 2020 +0200
+++ b/src/HOL/Parity.thy Sat Apr 25 13:26:24 2020 +0000
@@ -1509,6 +1509,30 @@
instance int :: unique_euclidean_semiring_with_bit_shifts ..
+lemma not_exp_less_eq_0_int [simp]:
+ \<open>\<not> 2 ^ n \<le> (0::int)\<close>
+ by (simp add: power_le_zero_eq)
+
+lemma half_nonnegative_int_iff [simp]:
+ \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+proof (cases \<open>k \<ge> 0\<close>)
+ case True
+ then show ?thesis
+ by (auto simp add: divide_int_def sgn_1_pos)
+next
+ case False
+ then show ?thesis
+ apply (auto simp add: divide_int_def not_le elim!: evenE)
+ apply (simp only: minus_mult_right)
+ apply (subst nat_mult_distrib)
+ apply simp_all
+ done
+qed
+
+lemma half_negative_int_iff [simp]:
+ \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
lemma push_bit_of_Suc_0 [simp]:
"push_bit n (Suc 0) = 2 ^ n"
using push_bit_of_1 [where ?'a = nat] by simp
@@ -1573,6 +1597,22 @@
lemma drop_bit_push_bit_int:
\<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
by (cases \<open>m \<le> n\<close>) (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
- mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add)
+ mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add)
+
+lemma push_bit_nonnegative_int_iff [simp]:
+ \<open>push_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by (simp add: push_bit_eq_mult zero_le_mult_iff)
+
+lemma push_bit_negative_int_iff [simp]:
+ \<open>push_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
+lemma drop_bit_nonnegative_int_iff [simp]:
+ \<open>drop_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by (induction n) (simp_all add: drop_bit_Suc drop_bit_half)
+
+lemma drop_bit_negative_int_iff [simp]:
+ \<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (subst Not_eq_iff [symmetric]) (simp add: not_less)
end
--- a/src/HOL/ex/Bit_Operations.thy Sat Apr 25 16:31:43 2020 +0200
+++ b/src/HOL/ex/Bit_Operations.thy Sat Apr 25 13:26:24 2020 +0000
@@ -160,6 +160,14 @@
done
qed
+lemma and_eq_not_not_or:
+ \<open>a AND b = NOT (NOT a OR NOT b)\<close>
+ by simp
+
+lemma or_eq_not_not_and:
+ \<open>a OR b = NOT (NOT a AND NOT b)\<close>
+ by simp
+
lemma push_bit_minus:
\<open>push_bit n (- a) = - push_bit n a\<close>
by (simp add: push_bit_eq_mult)
@@ -460,7 +468,8 @@
by (simp add: rec [of k l] bit_Suc)
qed
-sublocale abel_semigroup F
+lemma abel_semigroup_axioms:
+ \<open>abel_semigroup F\<close>
by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
end
@@ -468,30 +477,6 @@
instantiation int :: ring_bit_operations
begin
-global_interpretation and_int: zip_int "(\<and>)"
- defines and_int = and_int.F
- by standard
-
-global_interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
-proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
- show "k AND k = k" for k :: int
- by (simp add: bit_eq_iff and_int.bit_eq_iff)
-qed
-
-global_interpretation or_int: zip_int "(\<or>)"
- defines or_int = or_int.F
- by standard
-
-global_interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
-proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
- show "k OR k = k" for k :: int
- by (simp add: bit_eq_iff or_int.bit_eq_iff)
-qed
-
-global_interpretation xor_int: zip_int "(\<noteq>)"
- defines xor_int = xor_int.F
- by standard
-
definition not_int :: \<open>int \<Rightarrow> int\<close>
where \<open>not_int k = - k - 1\<close>
@@ -512,6 +497,30 @@
for k :: int
by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc)
+global_interpretation and_int: zip_int "(\<and>)"
+ defines and_int = and_int.F
+ by standard
+
+interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
+proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
+ show "k AND k = k" for k :: int
+ by (simp add: bit_eq_iff and_int.bit_eq_iff)
+qed
+
+global_interpretation or_int: zip_int "(\<or>)"
+ defines or_int = or_int.F
+ by standard
+
+interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
+proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
+ show "k OR k = k" for k :: int
+ by (simp add: bit_eq_iff or_int.bit_eq_iff)
+qed
+
+global_interpretation xor_int: zip_int "(\<noteq>)"
+ defines xor_int = xor_int.F
+ by standard
+
instance proof
fix k l :: int and n :: nat
show \<open>- k = NOT (k - 1)\<close>
@@ -526,6 +535,83 @@
end
+lemma not_nonnegative_int_iff [simp]:
+ \<open>NOT k \<ge> 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (simp add: not_int_def)
+
+lemma not_negative_int_iff [simp]:
+ \<open>NOT k < 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by (subst Not_eq_iff [symmetric]) (simp add: not_less not_le)
+
+lemma and_nonnegative_int_iff [simp]:
+ \<open>k AND l \<ge> 0 \<longleftrightarrow> k \<ge> 0 \<or> l \<ge> 0\<close> for k l :: int
+proof (induction k arbitrary: l rule: int_bit_induct)
+ case zero
+ then show ?case
+ by simp
+next
+ case minus
+ then show ?case
+ by simp
+next
+ case (even k)
+ then show ?case
+ using and_int.rec [of \<open>k * 2\<close> l] by (simp add: pos_imp_zdiv_nonneg_iff)
+next
+ case (odd k)
+ from odd have \<open>0 \<le> k AND l div 2 \<longleftrightarrow> 0 \<le> k \<or> 0 \<le> l div 2\<close>
+ by simp
+ then have \<open>0 \<le> (1 + k * 2) div 2 AND l div 2 \<longleftrightarrow> 0 \<le> (1 + k * 2) div 2\<or> 0 \<le> l div 2\<close>
+ by simp
+ with and_int.rec [of \<open>1 + k * 2\<close> l]
+ show ?case
+ by auto
+qed
+
+lemma and_negative_int_iff [simp]:
+ \<open>k AND l < 0 \<longleftrightarrow> k < 0 \<and> l < 0\<close> for k l :: int
+ by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
+lemma or_nonnegative_int_iff [simp]:
+ \<open>k OR l \<ge> 0 \<longleftrightarrow> k \<ge> 0 \<and> l \<ge> 0\<close> for k l :: int
+ by (simp only: or_eq_not_not_and not_nonnegative_int_iff) simp
+
+lemma or_negative_int_iff [simp]:
+ \<open>k OR l < 0 \<longleftrightarrow> k < 0 \<or> l < 0\<close> for k l :: int
+ by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
+lemma xor_nonnegative_int_iff [simp]:
+ \<open>k XOR l \<ge> 0 \<longleftrightarrow> (k \<ge> 0 \<longleftrightarrow> l \<ge> 0)\<close> for k l :: int
+ by (simp only: bit.xor_def or_nonnegative_int_iff) auto
+
+lemma xor_negative_int_iff [simp]:
+ \<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> for k l :: int
+ by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)
+
+lemma set_bit_nonnegative_int_iff [simp]:
+ \<open>set_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by (simp add: set_bit_def)
+
+lemma set_bit_negative_int_iff [simp]:
+ \<open>set_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (simp add: set_bit_def)
+
+lemma unset_bit_nonnegative_int_iff [simp]:
+ \<open>unset_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by (simp add: unset_bit_def)
+
+lemma unset_bit_negative_int_iff [simp]:
+ \<open>unset_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (simp add: unset_bit_def)
+
+lemma flip_bit_nonnegative_int_iff [simp]:
+ \<open>flip_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by (simp add: flip_bit_def)
+
+lemma flip_bit_negative_int_iff [simp]:
+ \<open>flip_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by (simp add: flip_bit_def)
+
subsubsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close>
@@ -609,8 +695,6 @@
subsection \<open>Key ideas of bit operations\<close>
-subsection \<open>Key ideas of bit operations\<close>
-
text \<open>
When formalizing bit operations, it is tempting to represent
bit values as explicit lists over a binary type. This however