src/HOL/Ring_and_Field.thy
changeset 25512 4134f7c782e2
parent 25450 c3b26e533b21
child 25564 4ca31a3706a4
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Nov 30 20:13:05 2007 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Nov 30 20:13:06 2007 +0100
     1.3 @@ -80,14 +80,14 @@
     1.4  class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
     1.5  begin
     1.6  
     1.7 -subclass semiring_0 by unfold_locales
     1.8 +subclass semiring_0 by intro_locales
     1.9  
    1.10  end
    1.11  
    1.12  class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
    1.13  begin
    1.14  
    1.15 -subclass semiring_0_cancel by unfold_locales
    1.16 +subclass semiring_0_cancel by intro_locales
    1.17  
    1.18  end
    1.19  
    1.20 @@ -100,7 +100,7 @@
    1.21    (*previously almost_semiring*)
    1.22  begin
    1.23  
    1.24 -subclass semiring_1 by unfold_locales
    1.25 +subclass semiring_1 by intro_locales
    1.26  
    1.27  end
    1.28  
    1.29 @@ -111,9 +111,9 @@
    1.30    + cancel_ab_semigroup_add + monoid_mult
    1.31  begin
    1.32  
    1.33 -subclass semiring_0_cancel by unfold_locales
    1.34 -
    1.35 -subclass semiring_1 by unfold_locales
    1.36 +subclass semiring_0_cancel by intro_locales
    1.37 +
    1.38 +subclass semiring_1 by intro_locales
    1.39  
    1.40  end
    1.41  
    1.42 @@ -121,16 +121,16 @@
    1.43    + zero_neq_one + cancel_ab_semigroup_add
    1.44  begin
    1.45  
    1.46 -subclass semiring_1_cancel by unfold_locales
    1.47 -subclass comm_semiring_0_cancel by unfold_locales
    1.48 -subclass comm_semiring_1 by unfold_locales
    1.49 +subclass semiring_1_cancel by intro_locales
    1.50 +subclass comm_semiring_0_cancel by intro_locales
    1.51 +subclass comm_semiring_1 by intro_locales
    1.52  
    1.53  end
    1.54  
    1.55  class ring = semiring + ab_group_add
    1.56  begin
    1.57  
    1.58 -subclass semiring_0_cancel by unfold_locales
    1.59 +subclass semiring_0_cancel by intro_locales
    1.60  
    1.61  text {* Distribution rules *}
    1.62  
    1.63 @@ -179,15 +179,15 @@
    1.64  class comm_ring = comm_semiring + ab_group_add
    1.65  begin
    1.66  
    1.67 -subclass ring by unfold_locales
    1.68 -subclass comm_semiring_0 by unfold_locales
    1.69 +subclass ring by intro_locales
    1.70 +subclass comm_semiring_0 by intro_locales
    1.71  
    1.72  end
    1.73  
    1.74  class ring_1 = ring + zero_neq_one + monoid_mult
    1.75  begin
    1.76  
    1.77 -subclass semiring_1_cancel by unfold_locales
    1.78 +subclass semiring_1_cancel by intro_locales
    1.79  
    1.80  end
    1.81  
    1.82 @@ -195,8 +195,8 @@
    1.83    (*previously ring*)
    1.84  begin
    1.85  
    1.86 -subclass ring_1 by unfold_locales
    1.87 -subclass comm_semiring_1_cancel by unfold_locales
    1.88 +subclass ring_1 by intro_locales
    1.89 +subclass comm_semiring_1_cancel by intro_locales
    1.90  
    1.91  end
    1.92  
    1.93 @@ -219,7 +219,7 @@
    1.94  class idom = comm_ring_1 + no_zero_divisors
    1.95  begin
    1.96  
    1.97 -subclass ring_1_no_zero_divisors by unfold_locales
    1.98 +subclass ring_1_no_zero_divisors by intro_locales
    1.99  
   1.100  end
   1.101  
   1.102 @@ -261,7 +261,7 @@
   1.103    thus "a * inverse a = 1" by (simp only: mult_commute)
   1.104  qed
   1.105  
   1.106 -subclass idom by unfold_locales
   1.107 +subclass idom by intro_locales
   1.108  
   1.109  lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
   1.110  proof
   1.111 @@ -331,8 +331,8 @@
   1.112    + semiring + comm_monoid_add + cancel_ab_semigroup_add
   1.113  begin
   1.114  
   1.115 -subclass semiring_0_cancel by unfold_locales
   1.116 -subclass pordered_semiring by unfold_locales
   1.117 +subclass semiring_0_cancel by intro_locales
   1.118 +subclass pordered_semiring by intro_locales
   1.119  
   1.120  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   1.121    by (drule mult_left_mono [of zero b], auto)
   1.122 @@ -351,9 +351,9 @@
   1.123  class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   1.124  begin
   1.125  
   1.126 -subclass pordered_cancel_semiring by unfold_locales
   1.127 -
   1.128 -subclass pordered_comm_monoid_add by unfold_locales
   1.129 +subclass pordered_cancel_semiring by intro_locales
   1.130 +
   1.131 +subclass pordered_comm_monoid_add by intro_locales
   1.132  
   1.133  lemma mult_left_less_imp_less:
   1.134    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   1.135 @@ -370,7 +370,7 @@
   1.136    assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   1.137  begin
   1.138  
   1.139 -subclass semiring_0_cancel by unfold_locales
   1.140 +subclass semiring_0_cancel by intro_locales
   1.141  
   1.142  subclass ordered_semiring
   1.143  proof unfold_locales
   1.144 @@ -443,8 +443,8 @@
   1.145    + pordered_ab_semigroup_add + mult_mono1
   1.146  begin
   1.147  
   1.148 -subclass pordered_comm_semiring by unfold_locales
   1.149 -subclass pordered_cancel_semiring by unfold_locales
   1.150 +subclass pordered_comm_semiring by intro_locales
   1.151 +subclass pordered_cancel_semiring by intro_locales
   1.152  
   1.153  end
   1.154  
   1.155 @@ -474,7 +474,7 @@
   1.156  class pordered_ring = ring + pordered_cancel_semiring 
   1.157  begin
   1.158  
   1.159 -subclass pordered_ab_group_add by unfold_locales
   1.160 +subclass pordered_ab_group_add by intro_locales
   1.161  
   1.162  lemmas ring_simps = ring_simps group_simps
   1.163  
   1.164 @@ -526,7 +526,7 @@
   1.165    + ordered_ab_group_add + abs_if
   1.166  begin
   1.167  
   1.168 -subclass pordered_ring by unfold_locales
   1.169 +subclass pordered_ring by intro_locales
   1.170  
   1.171  subclass pordered_ab_group_add_abs
   1.172  proof unfold_locales
   1.173 @@ -547,7 +547,7 @@
   1.174    + ordered_ab_group_add + abs_if
   1.175  begin
   1.176  
   1.177 -subclass ordered_ring by unfold_locales
   1.178 +subclass ordered_ring by intro_locales
   1.179  
   1.180  lemma mult_strict_left_mono_neg:
   1.181    "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   1.182 @@ -614,8 +614,8 @@
   1.183  class pordered_comm_ring = comm_ring + pordered_comm_semiring
   1.184  begin
   1.185  
   1.186 -subclass pordered_ring by unfold_locales
   1.187 -subclass pordered_cancel_comm_semiring by unfold_locales
   1.188 +subclass pordered_ring by intro_locales
   1.189 +subclass pordered_cancel_comm_semiring by intro_locales
   1.190  
   1.191  end
   1.192  
   1.193 @@ -2017,8 +2017,8 @@
   1.194  class lordered_ring = pordered_ring + lordered_ab_group_add_abs
   1.195  begin
   1.196  
   1.197 -subclass lordered_ab_group_add_meet by unfold_locales
   1.198 -subclass lordered_ab_group_add_join by unfold_locales
   1.199 +subclass lordered_ab_group_add_meet by intro_locales
   1.200 +subclass lordered_ab_group_add_join by intro_locales
   1.201  
   1.202  end
   1.203