axclass ordered_ring;
authorwenzelm
Sat Nov 18 19:47:12 2000 +0100 (2000-11-18 ago)
changeset 10492107c7db021a9
parent 10491 e4a408728012
child 10493 76e05ec87b57
axclass ordered_ring;
instance int :: ordered_ring;
src/HOL/Library/Ring_and_Field.thy
     1.1 --- a/src/HOL/Library/Ring_and_Field.thy	Sat Nov 18 19:46:48 2000 +0100
     1.2 +++ b/src/HOL/Library/Ring_and_Field.thy	Sat Nov 18 19:47:12 2000 +0100
     1.3 @@ -10,16 +10,14 @@
     1.4  
     1.5  theory Ring_and_Field = Main: 
     1.6  
     1.7 -text {*
     1.8 - The class @{text ring} models commutative ring structures with $1$.
     1.9 -*}
    1.10 +subsection {* Abstract algebraic structures *}
    1.11  
    1.12  axclass ring < zero, plus, minus, times, number
    1.13    add_assoc: "(a + b) + c = a + (b + c)"
    1.14    add_commute: "a + b = b + a"
    1.15    left_zero: "0 + a = a"
    1.16 -  left_minus: "(- a) + a = 0"
    1.17 -  diff_minus: "a - b = a + (- b)"
    1.18 +  left_minus: "(-a) + a = 0"
    1.19 +  diff_minus: "a - b = a + (-b)"
    1.20    zero_number: "0 = #0"
    1.21  
    1.22    mult_assoc: "(a * b) * c = a * (b * c)"
    1.23 @@ -28,14 +26,36 @@
    1.24  
    1.25    left_distrib: "(a + b) * c = a * c + b * c"
    1.26  
    1.27 +axclass ordered_ring < ring, linorder
    1.28 +  add_left_mono: "a \<le> b ==> c + a \<le> c + b"
    1.29 +  mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
    1.30 +  abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
    1.31  
    1.32  axclass field < ring, inverse
    1.33    left_inverse: "a \<noteq> 0 ==> inverse a * a = #1"
    1.34    divides_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
    1.35  
    1.36 +axclass ordered_field < ordered_ring, field
    1.37  
    1.38 -axclass ordered_field < field, linorder
    1.39 -  add_left_mono: "a \<le> b ==> c + a \<le> c + b"
    1.40 -  mult_left_mono: "a \<le> b ==> 0 < c ==> c * a \<le> c * b"
    1.41 +
    1.42 +subsection {* The ordered ring of integers *}
    1.43 +
    1.44 +instance int :: ordered_ring
    1.45 +proof
    1.46 +  fix i j k :: int
    1.47 +  show "(i + j) + k = i + (j + k)" by simp
    1.48 +  show "i + j = j + i" by simp
    1.49 +  show "0 + i = i" by simp
    1.50 +  show "(-i) + i = 0" by simp
    1.51 +  show "i - j = i + (-j)" by simp
    1.52 +  show "(i * j) * k = i * (j * k)" by simp
    1.53 +  show "i * j = j * i" by simp
    1.54 +  show "#1 * i = i" by simp
    1.55 +  show "0 = (#0::int)" by simp
    1.56 +  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
    1.57 +  show "i \<le> j ==> k + i \<le> k + j" by simp
    1.58 +  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
    1.59 +  show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
    1.60 +qed
    1.61  
    1.62  end