src/HOL/Rings.thy
changeset 66816 212a3334e7da
parent 66810 cc2b490f9dc4
child 66937 a1a4a5e2933a
     1.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -118,6 +118,13 @@
     1.4  end
     1.5  
     1.6  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
     1.7 +begin
     1.8 +
     1.9 +lemma (in semiring_1) of_bool_conj:
    1.10 +  "of_bool (P \<and> Q) = of_bool P * of_bool Q"
    1.11 +  by auto
    1.12 +
    1.13 +end
    1.14  
    1.15  text \<open>Abstract divisibility\<close>
    1.16  
    1.17 @@ -2319,6 +2326,10 @@
    1.18      by (auto simp add: abs_mult)
    1.19  qed
    1.20  
    1.21 +lemma sgn_not_eq_imp:
    1.22 +  "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
    1.23 +  using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
    1.24 +
    1.25  lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
    1.26    by (simp add: abs_if)
    1.27