src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -118,6 +118,13 @@
 end
 
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
+begin
+
+lemma (in semiring_1) of_bool_conj:
+  "of_bool (P \<and> Q) = of_bool P * of_bool Q"
+  by auto
+
+end
 
 text \<open>Abstract divisibility\<close>
 
@@ -2319,6 +2326,10 @@
     by (auto simp add: abs_mult)
 qed
 
+lemma sgn_not_eq_imp:
+  "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
+  using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
+
 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)