src/HOL/Rings.thy
changeset 62347 2230b7047376
parent 61944 5d06ecfdb472
child 62349 7c23469b5118
     1.1 --- a/src/HOL/Rings.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -1562,6 +1562,14 @@
     1.4  proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
     1.5    by (auto simp add: abs_if split: split_if_asm)
     1.6  
     1.7 +lemma sum_squares_ge_zero:
     1.8 +  "0 \<le> x * x + y * y"
     1.9 +  by (intro add_nonneg_nonneg zero_le_square)
    1.10 +
    1.11 +lemma not_sum_squares_lt_zero:
    1.12 +  "\<not> x * x + y * y < 0"
    1.13 +  by (simp add: not_less sum_squares_ge_zero)
    1.14 +
    1.15  end
    1.16  
    1.17  class linordered_ring_strict = ring + linordered_semiring_strict
    1.18 @@ -1867,6 +1875,10 @@
    1.19    "sgn a < 0 \<longleftrightarrow> a < 0"
    1.20    unfolding sgn_if by auto
    1.21  
    1.22 +lemma abs_sgn_eq:
    1.23 +  "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
    1.24 +  by (simp add: sgn_if)
    1.25 +
    1.26  lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
    1.27    by (simp add: abs_if)
    1.28