src/HOL/Ring_and_Field.thy
changeset 14940 b9ab8babd8b3
parent 14770 fe9504ba63d5
child 15010 72fbe711e414
     1.1 --- a/src/HOL/Ring_and_Field.thy	Sun Jun 13 17:57:35 2004 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Jun 14 14:20:55 2004 +0200
     1.3 @@ -27,6 +27,8 @@
     1.4  
     1.5  axclass semiring_0 \<subseteq> semiring, comm_monoid_add
     1.6  
     1.7 +axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
     1.8 +
     1.9  axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
    1.10    mult_commute: "a * b = b * a"
    1.11    distrib: "(a + b) * c = a * c + b * c"
    1.12 @@ -45,6 +47,10 @@
    1.13  
    1.14  instance comm_semiring_0 \<subseteq> semiring_0 ..
    1.15  
    1.16 +axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
    1.17 +
    1.18 +instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
    1.19 +
    1.20  axclass axclass_0_neq_1 \<subseteq> zero, one
    1.21    zero_neq_one [simp]: "0 \<noteq> 1"
    1.22  
    1.23 @@ -57,20 +63,30 @@
    1.24  axclass axclass_no_zero_divisors \<subseteq> zero, times
    1.25    no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    1.26  
    1.27 +axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
    1.28 +
    1.29 +instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
    1.30 +
    1.31  axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
    1.32  
    1.33 +instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
    1.34 +
    1.35 +instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
    1.36 +
    1.37  axclass ring \<subseteq> semiring, ab_group_add
    1.38  
    1.39 -instance ring \<subseteq> semiring_0 ..
    1.40 +instance ring \<subseteq> semiring_0_cancel ..
    1.41  
    1.42  axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
    1.43  
    1.44  instance comm_ring \<subseteq> ring ..
    1.45  
    1.46 -instance comm_ring \<subseteq> comm_semiring_0 ..
    1.47 +instance comm_ring \<subseteq> comm_semiring_0_cancel ..
    1.48  
    1.49  axclass ring_1 \<subseteq> ring, semiring_1
    1.50  
    1.51 +instance ring_1 \<subseteq> semiring_1_cancel ..
    1.52 +
    1.53  axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
    1.54  
    1.55  instance comm_ring_1 \<subseteq> ring_1 ..
    1.56 @@ -83,7 +99,7 @@
    1.57    left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
    1.58    divide_inverse:      "a / b = a * inverse b"
    1.59  
    1.60 -lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})"
    1.61 +lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
    1.62  proof -
    1.63    have "0*a + 0*a = 0*a + 0"
    1.64      by (simp add: left_distrib [symmetric])
    1.65 @@ -91,7 +107,7 @@
    1.66      by (simp only: add_left_cancel)
    1.67  qed
    1.68  
    1.69 -lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})"
    1.70 +lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
    1.71  proof -
    1.72    have "a*0 + a*0 = a*0 + 0"
    1.73      by (simp add: right_distrib [symmetric])
    1.74 @@ -155,10 +171,14 @@
    1.75  
    1.76  axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
    1.77  
    1.78 +instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
    1.79 +
    1.80  axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
    1.81    mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    1.82    mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
    1.83  
    1.84 +instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
    1.85 +
    1.86  instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring
    1.87  apply intro_classes
    1.88  apply (case_tac "a < b & 0 < c")
    1.89 @@ -200,6 +220,10 @@
    1.90  
    1.91  axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
    1.92  
    1.93 +instance lordered_ring \<subseteq> lordered_ab_group_meet ..
    1.94 +
    1.95 +instance lordered_ring \<subseteq> lordered_ab_group_join ..
    1.96 +
    1.97  axclass axclass_abs_if \<subseteq> minus, ord, zero
    1.98    abs_if: "abs a = (if (a < 0) then (-a) else a)"
    1.99