# HG changeset patch
# User haftmann
# Date 1587821184 0
# Node ID ab3cecb836b557c0b1cf388ce9b29d61e57a89e1
# Parent  49d8d8ad7e431f01b82892a180d0d026c9cd2560
more rules

diff -r 49d8d8ad7e43 -r ab3cecb836b5 src/HOL/Parity.thy
--- 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
diff -r 49d8d8ad7e43 -r ab3cecb836b5 src/HOL/ex/Bit_Operations.thy
--- 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