# HG changeset patch
# User haftmann
# Date 1193313120 -7200
# Node ID f4d1ebffd0258c8f79a0fb50c6d3c29772ecf316
# Parent  762ed22d15c737b60698853c0f22d25c2b7e57cc
localized further

diff -r 762ed22d15c7 -r f4d1ebffd025 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Oct 25 13:51:58 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Oct 25 13:52:00 2007 +0200
@@ -42,9 +42,10 @@
 class semiring_0 = semiring + comm_monoid_add + mult_zero
 
 class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
+begin
 
-instance semiring_0_cancel \<subseteq> semiring_0
-proof
+subclass semiring_0
+proof unfold_locales
   fix a :: 'a
   have "0 * a + 0 * a = 0 * a + 0"
     by (simp add: left_distrib [symmetric])
@@ -58,20 +59,7 @@
     by (simp only: add_left_cancel)
 qed
 
-interpretation semiring_0_cancel \<subseteq> semiring_0
-proof unfold_locales
-  fix a :: 'a
-  have "plus (times zero a) (times zero a) = plus (times zero a) zero"
-    by (simp add: left_distrib [symmetric])
-  thus "times zero a = zero"
-    by (simp only: add_left_cancel)
-next
-  fix a :: 'a
-  have "plus (times a zero) (times a zero) = plus (times a zero) zero"
-    by (simp add: right_distrib [symmetric])
-  thus "times a zero = zero"
-    by (simp only: add_left_cancel)
-qed
+end
 
 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
   assumes distrib: "(a + b) * c = a * c + b * c"
@@ -97,10 +85,11 @@
 end
 
 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
+begin
 
-instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
+subclass semiring_0_cancel by unfold_locales
 
-interpretation comm_semiring_0_cancel \<subseteq> semiring_0_cancel by unfold_locales
+end
 
 class zero_neq_one = zero + one +
   assumes zero_neq_one [simp]: "0 \<noteq> 1"
@@ -121,30 +110,20 @@
 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
   + cancel_ab_semigroup_add + monoid_mult
 
-instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
-
-interpretation semiring_1_cancel \<subseteq> semiring_0_cancel by unfold_locales
+subclass (in semiring_1_cancel) semiring_0_cancel by unfold_locales
 
 subclass (in semiring_1_cancel) semiring_1 by unfold_locales
 
 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
   + zero_neq_one + cancel_ab_semigroup_add
 
-instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
-
-interpretation comm_semiring_1_cancel \<subseteq> semiring_1_cancel by unfold_locales
-
+subclass (in comm_semiring_1_cancel) semiring_1_cancel by unfold_locales
 subclass (in comm_semiring_1_cancel) comm_semiring_0_cancel by unfold_locales
-
-instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
-
-interpretation comm_semiring_1_cancel \<subseteq> comm_semiring_1 by unfold_locales
+subclass (in comm_semiring_1_cancel) comm_semiring_1 by unfold_locales
 
 class ring = semiring + ab_group_add
 
-instance ring \<subseteq> semiring_0_cancel ..
-
-interpretation ring \<subseteq> semiring_0_cancel by unfold_locales
+subclass (in ring) semiring_0_cancel by unfold_locales
 
 context ring
 begin
@@ -187,47 +166,37 @@
 
 class comm_ring = comm_semiring + ab_group_add
 
-instance comm_ring \<subseteq> ring ..
-
-interpretation comm_ring \<subseteq> ring by unfold_locales
-
-instance comm_ring \<subseteq> comm_semiring_0 ..
-
-interpretation comm_ring \<subseteq> comm_semiring_0 by unfold_locales
+subclass (in comm_ring) ring by unfold_locales
+subclass (in comm_ring) comm_semiring_0 by unfold_locales
 
 class ring_1 = ring + zero_neq_one + monoid_mult
 
-instance ring_1 \<subseteq> semiring_1_cancel ..
-
-interpretation ring_1 \<subseteq> semiring_1_cancel by unfold_locales
+subclass (in ring_1) semiring_1_cancel by unfold_locales
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   (*previously ring*)
 
-instance comm_ring_1 \<subseteq> ring_1 ..
-
-interpretation comm_ring_1 \<subseteq> ring_1 by unfold_locales
-
-instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
-
-interpretation comm_ring_1 \<subseteq> comm_semiring_1_cancel by unfold_locales
+subclass (in comm_ring_1) ring_1 by unfold_locales
+subclass (in comm_ring_1) comm_semiring_1_cancel by unfold_locales
 
 class ring_no_zero_divisors = ring + no_zero_divisors
 
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 
 class idom = comm_ring_1 + no_zero_divisors
+begin
 
-instance idom \<subseteq> ring_1_no_zero_divisors ..
+subclass ring_1_no_zero_divisors by unfold_locales
 
-interpretation idom \<subseteq> ring_1_no_zero_divisors by unfold_locales
+end
 
 class division_ring = ring_1 + inverse +
   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
+begin
 
-instance division_ring \<subseteq> ring_1_no_zero_divisors
-proof
+subclass ring_1_no_zero_divisors
+proof unfold_locales
   fix a b :: 'a
   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   show "a * b \<noteq> 0"
@@ -244,44 +213,19 @@
   qed
 qed
 
-interpretation division_ring \<subseteq> ring_1_no_zero_divisors
-proof unfold_locales
-  fix a b :: 'a
-  assume a: "a \<noteq> zero" and b: "b \<noteq> zero"
-  show "times a b \<noteq> zero"
-  proof
-    assume ab: "times a b = zero"
-    hence "zero = times (times (inverse a) (times a b)) (inverse b)"
-      by simp
-    also have "\<dots> = times (times (inverse a) a) (times b (inverse b))"
-      by (simp only: mult_assoc)
-    also have "\<dots> = one"
-      using a b by simp
-    finally show False
-      by simp
-  qed
-qed
+end
 
 class field = comm_ring_1 + inverse +
   assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   assumes divide_inverse: "a / b = a * inverse b"
 
-instance field \<subseteq> division_ring
-proof
+subclass (in field) division_ring
+proof unfold_locales
   fix a :: 'a
   assume "a \<noteq> 0"
   thus "inverse a * a = 1" by (rule field_inverse)
   thus "a * inverse a = 1" by (simp only: mult_commute)
 qed
-
-interpretation field \<subseteq> division_ring
-proof unfold_locales
-  fix a :: 'a
-  assume "a \<noteq> zero"
-  thus "times (inverse a) a = one" by (rule field_inverse)
-  thus "times a (inverse a) = one" by (simp only: mult_commute)
-qed
-
 subclass (in field) idom by unfold_locales
 
 class division_by_zero = zero + inverse +
@@ -296,48 +240,32 @@
 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   + semiring + comm_monoid_add + cancel_ab_semigroup_add
 
-instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
-
-interpretation pordered_cancel_semiring \<subseteq> semiring_0_cancel by unfold_locales
-
+subclass (in pordered_cancel_semiring) semiring_0_cancel by unfold_locales
 subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales
 
 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
+begin
 
-instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
+subclass pordered_cancel_semiring by unfold_locales
 
-interpretation ordered_semiring \<subseteq> pordered_cancel_semiring by unfold_locales
+end
 
 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 
-instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
+subclass (in ordered_semiring_strict) semiring_0_cancel by unfold_locales
 
-interpretation ordered_semiring_strict \<subseteq> semiring_0_cancel by unfold_locales
-
-instance ordered_semiring_strict \<subseteq> ordered_semiring
-proof
+subclass (in ordered_semiring_strict) ordered_semiring
+proof unfold_locales
   fix a b c :: 'a
   assume A: "a \<le> b" "0 \<le> c"
   from A show "c * a \<le> c * b"
-    unfolding order_le_less
-    using mult_strict_left_mono by auto
+    unfolding le_less
+    using mult_strict_left_mono by (cases "c = 0") auto
   from A show "a * c \<le> b * c"
-    unfolding order_le_less
-    using mult_strict_right_mono by auto
-qed
-
-interpretation ordered_semiring_strict \<subseteq> ordered_semiring
-proof unfold_locales
-  fix a b c :: 'a
-  assume A: "less_eq a b" "less_eq zero c"
-  from A show "less_eq (times c a) (times c b)"
-    unfolding le_less  
-    using mult_strict_left_mono by (cases "c = zero") auto
-  from A show "less_eq (times a c) (times b c)"
     unfolding le_less
-    using mult_strict_right_mono by (cases "c = zero") auto
+    using mult_strict_right_mono by (cases "c = 0") auto
 qed
 
 class mult_mono1 = times + zero + ord +
@@ -348,64 +276,70 @@
 
 class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   + pordered_ab_semigroup_add + mult_mono1
+begin
 
--- {*FIXME: continue localization here*}
+subclass pordered_comm_semiring by unfold_locales
 
-instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
+end
 
 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
 
-instance pordered_comm_semiring \<subseteq> pordered_semiring
-proof
+subclass (in pordered_comm_semiring) pordered_semiring
+proof unfold_locales
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
   thus "c * a \<le> c * b" by (rule mult_mono)
   thus "a * c \<le> b * c" by (simp only: mult_commute)
 qed
 
-instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
+subclass (in pordered_cancel_comm_semiring) pordered_cancel_semiring
+  by unfold_locales
 
-instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict
-proof
+subclass (in ordered_comm_semiring_strict) ordered_semiring_strict
+proof unfold_locales
   fix a b c :: 'a
   assume "a < b" "0 < c"
   thus "c * a < c * b" by (rule mult_strict_mono)
   thus "a * c < b * c" by (simp only: mult_commute)
 qed
 
-instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring
-proof
+subclass (in ordered_comm_semiring_strict) pordered_cancel_comm_semiring
+proof unfold_locales
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
   thus "c * a \<le> c * b"
-    unfolding order_le_less
-    using mult_strict_mono by auto
+    unfolding le_less
+    using mult_strict_mono by (cases "c = 0") auto
 qed
 
 class pordered_ring = ring + pordered_cancel_semiring 
+begin
 
-instance pordered_ring \<subseteq> pordered_ab_group_add ..
+subclass pordered_ab_group_add by unfold_locales
+
+end
 
 class lordered_ring = pordered_ring + lordered_ab_group_abs
 
-instance lordered_ring \<subseteq> lordered_ab_group_meet ..
-
-instance lordered_ring \<subseteq> lordered_ab_group_join ..
+subclass (in lordered_ring) lordered_ab_group_meet by unfold_locales
+subclass (in lordered_ring) lordered_ab_group_join by unfold_locales
 
 class abs_if = minus + ord + zero + abs +
-  assumes abs_if: "abs a = (if a < 0 then (uminus a) else a)"
+  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
 
 class sgn_if = sgn + zero + one + minus + ord +
-  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else uminus 1)"
+  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
 
 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
  *)
 class ordered_ring = ring + ordered_semiring + lordered_ab_group + abs_if
 
+-- {*FIXME: continue localization here*}
+
 instance ordered_ring \<subseteq> lordered_ring
-proof
+proof 
   fix x :: 'a
   show "\<bar>x\<bar> = sup x (- x)"
     by (simp only: abs_if sup_eq_if)