src/HOL/Ring_and_Field.thy

 end
 
 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
 begin
 
-subclass semiring_0 by unfold_locales
+subclass semiring_0 by intro_locales
 
 end
 
 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
 begin
 
-subclass semiring_0_cancel by unfold_locales
+subclass semiring_0_cancel by intro_locales
 
 end
 
 class zero_neq_one = zero + one +
   assumes zero_neq_one [simp]: "0 \<noteq> 1"

 
 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
   (*previously almost_semiring*)
 begin
 
-subclass semiring_1 by unfold_locales
+subclass semiring_1 by intro_locales
 
 end
 
 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
 begin
 
-subclass semiring_0_cancel by unfold_locales
-
-subclass semiring_1 by unfold_locales
+subclass semiring_0_cancel by intro_locales
+
+subclass semiring_1 by intro_locales
 
 end
 
 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
   + zero_neq_one + cancel_ab_semigroup_add
 begin
 
-subclass semiring_1_cancel by unfold_locales
-subclass comm_semiring_0_cancel by unfold_locales
-subclass comm_semiring_1 by unfold_locales
+subclass semiring_1_cancel by intro_locales
+subclass comm_semiring_0_cancel by intro_locales
+subclass comm_semiring_1 by intro_locales
 
 end
 
 class ring = semiring + ab_group_add
 begin
 
-subclass semiring_0_cancel by unfold_locales
+subclass semiring_0_cancel by intro_locales
 
 text {* Distribution rules *}
 
 lemma minus_mult_left: "- (a * b) = - a * b"
   by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 

   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
 begin
 
-subclass ring by unfold_locales
-subclass comm_semiring_0 by unfold_locales
+subclass ring by intro_locales
+subclass comm_semiring_0 by intro_locales
 
 end
 
 class ring_1 = ring + zero_neq_one + monoid_mult
 begin
 
-subclass semiring_1_cancel by unfold_locales
+subclass semiring_1_cancel by intro_locales
 
 end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   (*previously ring*)
 begin
 
-subclass ring_1 by unfold_locales
-subclass comm_semiring_1_cancel by unfold_locales
+subclass ring_1 by intro_locales
+subclass comm_semiring_1_cancel by intro_locales
 
 end
 
 class ring_no_zero_divisors = ring + no_zero_divisors
 begin

 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 
 class idom = comm_ring_1 + no_zero_divisors
 begin
 
-subclass ring_1_no_zero_divisors by unfold_locales
+subclass ring_1_no_zero_divisors by intro_locales
 
 end
 
 class division_ring = ring_1 + inverse +
   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"

   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 idom by unfold_locales
+subclass idom by intro_locales
 
 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
 proof
   assume neq: "b \<noteq> 0"
   {

 
 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   + semiring + comm_monoid_add + cancel_ab_semigroup_add
 begin
 
-subclass semiring_0_cancel by unfold_locales
-subclass pordered_semiring by unfold_locales
+subclass semiring_0_cancel by intro_locales
+subclass pordered_semiring by intro_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"

 end
 
 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
 begin
 
-subclass pordered_cancel_semiring by unfold_locales
-
-subclass pordered_comm_monoid_add by unfold_locales
+subclass pordered_cancel_semiring by intro_locales
+
+subclass pordered_comm_monoid_add by intro_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])
  

 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"
 begin
 
-subclass semiring_0_cancel by unfold_locales
+subclass semiring_0_cancel by intro_locales
 
 subclass ordered_semiring
 proof unfold_locales
   fix a b c :: 'a
   assume A: "a \<le> b" "0 \<le> c"

 
 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
+subclass pordered_comm_semiring by intro_locales
+subclass pordered_cancel_semiring by intro_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"

 end
 
 class pordered_ring = ring + pordered_cancel_semiring 
 begin
 
-subclass pordered_ab_group_add by unfold_locales
+subclass pordered_ab_group_add by intro_locales
 
 lemmas ring_simps = ring_simps group_simps
 
 lemma less_add_iff1:
   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"

 
 class ordered_ring = ring + ordered_semiring
   + ordered_ab_group_add + abs_if
 begin
 
-subclass pordered_ring by unfold_locales
+subclass pordered_ring by intro_locales
 
 subclass pordered_ab_group_add_abs
 proof unfold_locales
   fix a b
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

  *)
 class ordered_ring_strict = ring + ordered_semiring_strict
   + ordered_ab_group_add + abs_if
 begin
 
-subclass ordered_ring by unfold_locales
+subclass ordered_ring by intro_locales
 
 lemma mult_strict_left_mono_neg:
   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   apply (drule mult_strict_left_mono [of _ _ "uminus c"])
   apply (simp_all add: minus_mult_left [symmetric]) 

 
 
 class pordered_comm_ring = comm_ring + pordered_comm_semiring
 begin
 
-subclass pordered_ring by unfold_locales
-subclass pordered_cancel_comm_semiring by unfold_locales
+subclass pordered_ring by intro_locales
+subclass pordered_cancel_comm_semiring by intro_locales
 
 end
 
 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   (*previously ordered_semiring*)

 
 
 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
 begin
 
-subclass lordered_ab_group_add_meet by unfold_locales
-subclass lordered_ab_group_add_join by unfold_locales
+subclass lordered_ab_group_add_meet by intro_locales
+subclass lordered_ab_group_add_join by intro_locales
 
 end
 
 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
 proof -