src/HOL/Ring_and_Field.thy
changeset 14348 744c868ee0b7
parent 14341 a09441bd4f1e
child 14353 79f9fbef9106
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jan 09 01:28:24 2004 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Jan 09 10:46:18 2004 +0100
     1.3 @@ -38,6 +38,7 @@
     1.4    diff_minus: "a - b = a + (-b)"
     1.5  
     1.6  axclass ordered_semiring \<subseteq> semiring, linorder
     1.7 +  zero_less_one: "0 < 1" --{*This axiom too is needed for semirings only.*}
     1.8    add_left_mono: "a \<le> b ==> c + a \<le> c + b"
     1.9    mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
    1.10  
    1.11 @@ -484,6 +485,22 @@
    1.12       "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
    1.13    by (simp add: mult_left_mono mult_commute [of _ c]) 
    1.14  
    1.15 +lemma mult_left_le_imp_le:
    1.16 +     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
    1.17 +  by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
    1.18 + 
    1.19 +lemma mult_right_le_imp_le:
    1.20 +     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
    1.21 +  by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
    1.22 +
    1.23 +lemma mult_left_less_imp_less:
    1.24 +     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
    1.25 +  by (force simp add: mult_left_mono linorder_not_le [symmetric])
    1.26 + 
    1.27 +lemma mult_right_less_imp_less:
    1.28 +     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
    1.29 +  by (force simp add: mult_right_mono linorder_not_le [symmetric])
    1.30 +
    1.31  lemma mult_strict_left_mono_neg:
    1.32       "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
    1.33  apply (drule mult_strict_left_mono [of _ _ "-c"])
    1.34 @@ -552,12 +569,7 @@
    1.35  lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
    1.36  by (simp add: zero_le_mult_iff linorder_linear) 
    1.37  
    1.38 -lemma zero_less_one: "(0::'a::ordered_ring) < 1"
    1.39 -apply (insert zero_le_square [of 1]) 
    1.40 -apply (simp add: order_less_le) 
    1.41 -done
    1.42 -
    1.43 -lemma zero_le_one: "(0::'a::ordered_ring) \<le> 1"
    1.44 +lemma zero_le_one: "(0::'a::ordered_semiring) \<le> 1"
    1.45    by (rule zero_less_one [THEN order_less_imp_le]) 
    1.46  
    1.47  
    1.48 @@ -708,7 +720,7 @@
    1.49  
    1.50  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
    1.51        of an ordering.*}
    1.52 -lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
    1.53 +lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
    1.54    proof cases
    1.55      assume "a=0" thus ?thesis by simp
    1.56    next
    1.57 @@ -733,7 +745,7 @@
    1.58      by (simp add: mult_assoc cnz)
    1.59    qed
    1.60  
    1.61 -lemma field_mult_cancel_right:
    1.62 +lemma field_mult_cancel_right [simp]:
    1.63       "(a*c = b*c) = (c = (0::'a::field) | a=b)"
    1.64    proof cases
    1.65      assume "c=0" thus ?thesis by simp
    1.66 @@ -742,7 +754,7 @@
    1.67      thus ?thesis by (force dest: field_mult_cancel_right_lemma)
    1.68    qed
    1.69  
    1.70 -lemma field_mult_cancel_left:
    1.71 +lemma field_mult_cancel_left [simp]:
    1.72       "(c*a = c*b) = (c = (0::'a::field) | a=b)"
    1.73    by (simp add: mult_commute [of c] field_mult_cancel_right) 
    1.74  
    1.75 @@ -1401,6 +1413,10 @@
    1.76                    minus_mult_left [symmetric] minus_mult_right [symmetric])  
    1.77  done
    1.78  
    1.79 +
    1.80 +lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
    1.81 +by (simp add: abs_if) 
    1.82 +
    1.83  lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
    1.84  by (simp add: abs_if)
    1.85  
    1.86 @@ -1617,6 +1633,10 @@
    1.87  val mult_strict_right_mono = thm"mult_strict_right_mono";
    1.88  val mult_left_mono = thm"mult_left_mono";
    1.89  val mult_right_mono = thm"mult_right_mono";
    1.90 +val mult_left_le_imp_le = thm"mult_left_le_imp_le";
    1.91 +val mult_right_le_imp_le = thm"mult_right_le_imp_le";
    1.92 +val mult_left_less_imp_less = thm"mult_left_less_imp_less";
    1.93 +val mult_right_less_imp_less = thm"mult_right_less_imp_less";
    1.94  val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg";
    1.95  val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg";
    1.96  val mult_pos = thm"mult_pos";
    1.97 @@ -1744,6 +1764,7 @@
    1.98  val abs_zero = thm"abs_zero";
    1.99  val abs_one = thm"abs_one";
   1.100  val abs_mult = thm"abs_mult";
   1.101 +val abs_mult_self = thm"abs_mult_self";
   1.102  val abs_eq_0 = thm"abs_eq_0";
   1.103  val zero_less_abs_iff = thm"zero_less_abs_iff";
   1.104  val abs_not_less_zero = thm"abs_not_less_zero";