src/HOL/Ring_and_Field.thy

 class no_zero_divisors = zero + times +
   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
   + cancel_ab_semigroup_add + monoid_mult
-
-subclass (in semiring_1_cancel) semiring_0_cancel by unfold_locales
-
-subclass (in semiring_1_cancel) semiring_1 by unfold_locales
+begin
+
+subclass semiring_0_cancel by unfold_locales
+
+subclass semiring_1 by unfold_locales
+
+end
 
 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
   + zero_neq_one + cancel_ab_semigroup_add
-
-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
-subclass (in comm_semiring_1_cancel) comm_semiring_1 by unfold_locales
+begin
+
+subclass semiring_1_cancel by unfold_locales
+subclass comm_semiring_0_cancel by unfold_locales
+subclass comm_semiring_1 by unfold_locales
+
+end
 
 class ring = semiring + ab_group_add
-
-subclass (in ring) semiring_0_cancel by unfold_locales
-
-context ring
-begin
+begin
+
+subclass semiring_0_cancel by unfold_locales
 
 text {* Distribution rules *}
 
 lemma minus_mult_left: "- (a * b) = - a * b"
   by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 

 
 lemmas ring_distribs =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
-
-subclass (in comm_ring) ring by unfold_locales
-subclass (in comm_ring) comm_semiring_0 by unfold_locales
+begin
+
+subclass ring by unfold_locales
+subclass comm_semiring_0 by unfold_locales
+
+end
 
 class ring_1 = ring + zero_neq_one + monoid_mult
-
-subclass (in ring_1) semiring_1_cancel by unfold_locales
+begin
+
+subclass semiring_1_cancel by unfold_locales
+
+end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   (*previously ring*)
-
-subclass (in comm_ring_1) ring_1 by unfold_locales
-subclass (in comm_ring_1) comm_semiring_1_cancel by unfold_locales
+begin
+
+subclass ring_1 by unfold_locales
+subclass comm_semiring_1_cancel by unfold_locales
+
+end
 
 class ring_no_zero_divisors = ring + no_zero_divisors
 begin
 
 lemma mult_eq_0_iff [simp]:

 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"
-
-subclass (in field) division_ring
+begin
+
+subclass 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
 
-subclass (in field) idom by unfold_locales
-
-context field
-begin
+subclass idom by unfold_locales
 
 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
 proof
   assume neq: "b \<noteq> 0"
   {

 
 end
 
 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   + semiring + comm_monoid_add + cancel_ab_semigroup_add
-
-subclass (in pordered_cancel_semiring) semiring_0_cancel by unfold_locales
-subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales
-
-context pordered_cancel_semiring
-begin
+begin
+
+subclass semiring_0_cancel by unfold_locales
+subclass pordered_semiring by unfold_locales
 
 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   by (drule mult_left_mono [of zero b], auto)
 
 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"

   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
 
 end
 
 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
-
-subclass (in ordered_semiring) pordered_cancel_semiring by unfold_locales
-
-context ordered_semiring
-begin
+begin
+
+subclass pordered_cancel_semiring by unfold_locales
 
 lemma mult_left_less_imp_less:
   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   by (force simp add: mult_left_mono not_le [symmetric])
  

 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"
-
-subclass (in ordered_semiring_strict) semiring_0_cancel by unfold_locales
-
-subclass (in ordered_semiring_strict) ordered_semiring
+begin
+
+subclass semiring_0_cancel by unfold_locales
+
+subclass 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 le_less

   from A show "a * c \<le> b * c"
     unfolding le_less
     using mult_strict_right_mono by (cases "c = 0") auto
 qed
 
-context ordered_semiring_strict
-begin
-
 lemma mult_left_le_imp_le:
   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   by (force simp add: mult_strict_left_mono _not_less [symmetric])
  
 lemma mult_right_le_imp_le:

 class mult_mono1 = times + zero + ord +
   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
 
 class pordered_comm_semiring = comm_semiring_0
   + pordered_ab_semigroup_add + mult_mono1
-
-class pordered_cancel_comm_semiring = comm_semiring_0_cancel
-  + pordered_ab_semigroup_add + mult_mono1
-begin
-
-subclass pordered_comm_semiring by unfold_locales
-
-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"
-
-subclass (in pordered_comm_semiring) pordered_semiring
+begin
+
+subclass 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_mono1)
   thus "a * c \<le> b * c" by (simp only: mult_commute)
 qed
 
-subclass (in pordered_cancel_comm_semiring) pordered_cancel_semiring
-  by unfold_locales
-
-subclass (in ordered_comm_semiring_strict) ordered_semiring_strict
+end
+
+class pordered_cancel_comm_semiring = comm_semiring_0_cancel
+  + pordered_ab_semigroup_add + mult_mono1
+begin
+
+subclass pordered_comm_semiring by unfold_locales
+subclass pordered_cancel_semiring by unfold_locales
+
+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"
+begin
+
+subclass 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
 
-subclass (in ordered_comm_semiring_strict) pordered_cancel_comm_semiring
+subclass 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 le_less
     using mult_strict_mono by (cases "c = 0") auto
 qed
 
+end
+
 class pordered_ring = ring + pordered_cancel_semiring 
-
-subclass (in pordered_ring) pordered_ab_group_add by unfold_locales
-
-context pordered_ring
-begin
+begin
+
+subclass pordered_ab_group_add by unfold_locales
 
 lemmas ring_simps = ring_simps group_simps
 
 lemma less_add_iff1:
   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"

   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
 
 end
 
 class lordered_ring = pordered_ring + lordered_ab_group_abs
-
-subclass (in lordered_ring) lordered_ab_group_meet by unfold_locales
-subclass (in lordered_ring) lordered_ab_group_join by unfold_locales
+begin
+
+subclass lordered_ab_group_meet by unfold_locales
+subclass lordered_ab_group_join by unfold_locales
+
+end
 
 class abs_if = minus + ord + zero + abs +
   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
 
 class sgn_if = sgn + zero + one + minus + ord +

 also helps with inequalities. *}
 lemmas ring_simps = group_simps ring_distribs
 
 
 class pordered_comm_ring = comm_ring + pordered_comm_semiring
-
-subclass (in pordered_comm_ring) pordered_ring by unfold_locales
-
-subclass (in pordered_comm_ring) pordered_cancel_comm_semiring by unfold_locales
+begin
+
+subclass pordered_ring by unfold_locales
+subclass pordered_cancel_comm_semiring by unfold_locales
+
+end
 
 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   (*previously ordered_semiring*)
   assumes zero_less_one [simp]: "0 < 1"
 begin