src/HOL/Ring_and_Field.thy
changeset 21199 2d83f93c3580
parent 20633 e98f59806244
child 21258 62f25a96f0c1
     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Nov 07 08:03:46 2006 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Nov 07 09:33:47 2006 +0100
     1.3 @@ -27,9 +27,27 @@
     1.4    left_distrib: "(a + b) * c = a * c + b * c"
     1.5    right_distrib: "a * (b + c) = a * b + a * c"
     1.6  
     1.7 -axclass semiring_0 \<subseteq> semiring, comm_monoid_add
     1.8 +axclass mult_zero \<subseteq> times, zero
     1.9 +  mult_zero_left [simp]: "0 * a = 0"
    1.10 +  mult_zero_right [simp]: "a * 0 = 0"
    1.11 +
    1.12 +axclass semiring_0 \<subseteq> semiring, comm_monoid_add, mult_zero
    1.13 +
    1.14 +axclass semiring_0_cancel \<subseteq> semiring, comm_monoid_add, cancel_ab_semigroup_add
    1.15  
    1.16 -axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
    1.17 +instance semiring_0_cancel \<subseteq> semiring_0
    1.18 +proof
    1.19 +  fix a :: 'a
    1.20 +  have "0 * a + 0 * a = 0 * a + 0"
    1.21 +    by (simp add: left_distrib [symmetric])
    1.22 +  thus "0 * a = 0"
    1.23 +    by (simp only: add_left_cancel)
    1.24 +
    1.25 +  have "a * 0 + a * 0 = a * 0 + 0"
    1.26 +    by (simp add: right_distrib [symmetric])
    1.27 +  thus "a * 0 = 0"
    1.28 +    by (simp only: add_left_cancel)
    1.29 +qed
    1.30  
    1.31  axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
    1.32    distrib: "(a + b) * c = a * c + b * c"
    1.33 @@ -44,14 +62,16 @@
    1.34    finally show "a * (b + c) = a * b + a * c" by blast
    1.35  qed
    1.36  
    1.37 -axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add
    1.38 +axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add, mult_zero
    1.39  
    1.40  instance comm_semiring_0 \<subseteq> semiring_0 ..
    1.41  
    1.42 -axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
    1.43 +axclass comm_semiring_0_cancel \<subseteq> comm_semiring, comm_monoid_add, cancel_ab_semigroup_add
    1.44  
    1.45  instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
    1.46  
    1.47 +instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
    1.48 +
    1.49  axclass zero_neq_one \<subseteq> zero, one
    1.50    zero_neq_one [simp]: "0 \<noteq> 1"
    1.51  
    1.52 @@ -64,31 +84,37 @@
    1.53  axclass no_zero_divisors \<subseteq> zero, times
    1.54    no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    1.55  
    1.56 -axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
    1.57 +axclass semiring_1_cancel \<subseteq> semiring, comm_monoid_add, zero_neq_one, cancel_ab_semigroup_add, monoid_mult
    1.58  
    1.59  instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
    1.60  
    1.61 -axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
    1.62 +instance semiring_1_cancel \<subseteq> semiring_1 ..
    1.63 +
    1.64 +axclass comm_semiring_1_cancel \<subseteq> 
    1.65 +  comm_semiring, comm_monoid_add, comm_monoid_mult,
    1.66 +  zero_neq_one, cancel_ab_semigroup_add
    1.67  
    1.68  instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
    1.69  
    1.70  instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
    1.71  
    1.72 +instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
    1.73 +
    1.74  axclass ring \<subseteq> semiring, ab_group_add
    1.75  
    1.76  instance ring \<subseteq> semiring_0_cancel ..
    1.77  
    1.78 -axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
    1.79 +axclass comm_ring \<subseteq> comm_semiring, ab_group_add
    1.80  
    1.81  instance comm_ring \<subseteq> ring ..
    1.82  
    1.83  instance comm_ring \<subseteq> comm_semiring_0_cancel ..
    1.84  
    1.85 -axclass ring_1 \<subseteq> ring, semiring_1
    1.86 +axclass ring_1 \<subseteq> ring, zero_neq_one, monoid_mult
    1.87  
    1.88  instance ring_1 \<subseteq> semiring_1_cancel ..
    1.89  
    1.90 -axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
    1.91 +axclass comm_ring_1 \<subseteq> comm_ring, zero_neq_one, comm_monoid_mult (* previously ring *)
    1.92  
    1.93  instance comm_ring_1 \<subseteq> ring_1 ..
    1.94  
    1.95 @@ -115,22 +141,6 @@
    1.96  instance field \<subseteq> division_ring
    1.97  by (intro_classes, erule field_left_inverse, erule field_right_inverse)
    1.98  
    1.99 -lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
   1.100 -proof -
   1.101 -  have "0*a + 0*a = 0*a + 0"
   1.102 -    by (simp add: left_distrib [symmetric])
   1.103 -  thus ?thesis 
   1.104 -    by (simp only: add_left_cancel)
   1.105 -qed
   1.106 -
   1.107 -lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
   1.108 -proof -
   1.109 -  have "a*0 + a*0 = a*0 + 0"
   1.110 -    by (simp add: right_distrib [symmetric])
   1.111 -  thus ?thesis 
   1.112 -    by (simp only: add_left_cancel)
   1.113 -qed
   1.114 -
   1.115  lemma field_mult_eq_0_iff [simp]:
   1.116    "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
   1.117  proof cases
   1.118 @@ -182,15 +192,22 @@
   1.119  by (simp add: left_distrib diff_minus 
   1.120                minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   1.121  
   1.122 -axclass pordered_semiring \<subseteq> semiring_0, pordered_ab_semigroup_add 
   1.123 +axclass mult_mono \<subseteq> times, zero, ord
   1.124    mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   1.125    mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"
   1.126  
   1.127 -axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
   1.128 +axclass pordered_semiring \<subseteq> mult_mono, semiring_0, pordered_ab_semigroup_add 
   1.129 +
   1.130 +axclass pordered_cancel_semiring \<subseteq> 
   1.131 +  mult_mono, pordered_ab_semigroup_add,
   1.132 +  semiring, comm_monoid_add, 
   1.133 +  pordered_ab_semigroup_add, cancel_ab_semigroup_add
   1.134  
   1.135  instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
   1.136  
   1.137 -axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
   1.138 +instance pordered_cancel_semiring \<subseteq> pordered_semiring .. 
   1.139 +
   1.140 +axclass ordered_semiring_strict \<subseteq> semiring, comm_monoid_add, ordered_cancel_ab_semigroup_add
   1.141    mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   1.142    mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   1.143  
   1.144 @@ -204,18 +221,30 @@
   1.145  apply (simp add: mult_strict_right_mono)
   1.146  done
   1.147  
   1.148 -axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add
   1.149 +axclass mult_mono1 \<subseteq> times, zero, ord
   1.150    mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   1.151  
   1.152 -axclass pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring, cancel_ab_semigroup_add
   1.153 +axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add, mult_mono1
   1.154  
   1.155 +axclass pordered_cancel_comm_semiring \<subseteq> 
   1.156 +  comm_semiring_0_cancel, pordered_ab_semigroup_add, mult_mono1
   1.157 +  
   1.158  instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
   1.159  
   1.160  axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add
   1.161    mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   1.162  
   1.163  instance pordered_comm_semiring \<subseteq> pordered_semiring
   1.164 -by (intro_classes, insert mult_mono, simp_all add: mult_commute, blast+)
   1.165 +proof
   1.166 +  fix a b c :: 'a
   1.167 +  assume A: "a <= b" "0 <= c"
   1.168 +  with mult_mono show "c * a <= c * b" .
   1.169 +
   1.170 +  from mult_commute have "a * c = c * a" ..
   1.171 +  also from mult_mono A have "\<dots> <= c * b" .
   1.172 +  also from mult_commute have "c * b = b * c" ..
   1.173 +  finally show "a * c <= b * c" .
   1.174 +qed
   1.175  
   1.176  instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
   1.177  
   1.178 @@ -229,12 +258,10 @@
   1.179  apply (auto simp add: mult_strict_left_mono order_le_less)
   1.180  done
   1.181  
   1.182 -axclass pordered_ring \<subseteq> ring, pordered_semiring 
   1.183 +axclass pordered_ring \<subseteq> ring, pordered_cancel_semiring 
   1.184  
   1.185  instance pordered_ring \<subseteq> pordered_ab_group_add ..
   1.186  
   1.187 -instance pordered_ring \<subseteq> pordered_cancel_semiring ..
   1.188 -
   1.189  axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
   1.190  
   1.191  instance lordered_ring \<subseteq> lordered_ab_group_meet ..