using intro_locales instead of unfold_locales if appropriate
authorhaftmann
Fri Nov 30 20:13:06 2007 +0100 (2007-11-30)
changeset 255124134f7c782e2
parent 25511 54db9b5080b8
child 25513 b7de6e23e143
using intro_locales instead of unfold_locales if appropriate
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Nov 30 20:13:05 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Nov 30 20:13:06 2007 +0100
     1.3 @@ -471,7 +471,7 @@
     1.4  begin
     1.5  
     1.6  subclass pordered_cancel_ab_semigroup_add
     1.7 -  by unfold_locales
     1.8 +  by intro_locales
     1.9  
    1.10  subclass pordered_ab_semigroup_add_imp_le
    1.11  proof unfold_locales
    1.12 @@ -483,7 +483,7 @@
    1.13  qed
    1.14  
    1.15  subclass pordered_comm_monoid_add
    1.16 -  by unfold_locales
    1.17 +  by intro_locales
    1.18  
    1.19  lemma max_diff_distrib_left:
    1.20    shows "max x y - z = max (x - z) (y - z)"
    1.21 @@ -629,7 +629,7 @@
    1.22  begin
    1.23  
    1.24  subclass ordered_ab_semigroup_add
    1.25 -  by unfold_locales
    1.26 +  by intro_locales
    1.27  
    1.28  subclass pordered_ab_semigroup_add_imp_le
    1.29  proof unfold_locales
    1.30 @@ -657,7 +657,7 @@
    1.31  begin
    1.32  
    1.33  subclass ordered_cancel_ab_semigroup_add 
    1.34 -  by unfold_locales
    1.35 +  by intro_locales
    1.36  
    1.37  lemma neg_less_eq_nonneg:
    1.38    "- a \<le> a \<longleftrightarrow> 0 \<le> a"
    1.39 @@ -946,8 +946,8 @@
    1.40  class lordered_ab_group_add = pordered_ab_group_add + lattice
    1.41  begin
    1.42  
    1.43 -subclass lordered_ab_group_add_meet by unfold_locales
    1.44 -subclass lordered_ab_group_add_join by unfold_locales
    1.45 +subclass lordered_ab_group_add_meet by intro_locales
    1.46 +subclass lordered_ab_group_add_join by intro_locales
    1.47  
    1.48  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
    1.49  
     2.1 --- a/src/HOL/Ring_and_Field.thy	Fri Nov 30 20:13:05 2007 +0100
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Nov 30 20:13:06 2007 +0100
     2.3 @@ -80,14 +80,14 @@
     2.4  class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
     2.5  begin
     2.6  
     2.7 -subclass semiring_0 by unfold_locales
     2.8 +subclass semiring_0 by intro_locales
     2.9  
    2.10  end
    2.11  
    2.12  class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
    2.13  begin
    2.14  
    2.15 -subclass semiring_0_cancel by unfold_locales
    2.16 +subclass semiring_0_cancel by intro_locales
    2.17  
    2.18  end
    2.19  
    2.20 @@ -100,7 +100,7 @@
    2.21    (*previously almost_semiring*)
    2.22  begin
    2.23  
    2.24 -subclass semiring_1 by unfold_locales
    2.25 +subclass semiring_1 by intro_locales
    2.26  
    2.27  end
    2.28  
    2.29 @@ -111,9 +111,9 @@
    2.30    + cancel_ab_semigroup_add + monoid_mult
    2.31  begin
    2.32  
    2.33 -subclass semiring_0_cancel by unfold_locales
    2.34 -
    2.35 -subclass semiring_1 by unfold_locales
    2.36 +subclass semiring_0_cancel by intro_locales
    2.37 +
    2.38 +subclass semiring_1 by intro_locales
    2.39  
    2.40  end
    2.41  
    2.42 @@ -121,16 +121,16 @@
    2.43    + zero_neq_one + cancel_ab_semigroup_add
    2.44  begin
    2.45  
    2.46 -subclass semiring_1_cancel by unfold_locales
    2.47 -subclass comm_semiring_0_cancel by unfold_locales
    2.48 -subclass comm_semiring_1 by unfold_locales
    2.49 +subclass semiring_1_cancel by intro_locales
    2.50 +subclass comm_semiring_0_cancel by intro_locales
    2.51 +subclass comm_semiring_1 by intro_locales
    2.52  
    2.53  end
    2.54  
    2.55  class ring = semiring + ab_group_add
    2.56  begin
    2.57  
    2.58 -subclass semiring_0_cancel by unfold_locales
    2.59 +subclass semiring_0_cancel by intro_locales
    2.60  
    2.61  text {* Distribution rules *}
    2.62  
    2.63 @@ -179,15 +179,15 @@
    2.64  class comm_ring = comm_semiring + ab_group_add
    2.65  begin
    2.66  
    2.67 -subclass ring by unfold_locales
    2.68 -subclass comm_semiring_0 by unfold_locales
    2.69 +subclass ring by intro_locales
    2.70 +subclass comm_semiring_0 by intro_locales
    2.71  
    2.72  end
    2.73  
    2.74  class ring_1 = ring + zero_neq_one + monoid_mult
    2.75  begin
    2.76  
    2.77 -subclass semiring_1_cancel by unfold_locales
    2.78 +subclass semiring_1_cancel by intro_locales
    2.79  
    2.80  end
    2.81  
    2.82 @@ -195,8 +195,8 @@
    2.83    (*previously ring*)
    2.84  begin
    2.85  
    2.86 -subclass ring_1 by unfold_locales
    2.87 -subclass comm_semiring_1_cancel by unfold_locales
    2.88 +subclass ring_1 by intro_locales
    2.89 +subclass comm_semiring_1_cancel by intro_locales
    2.90  
    2.91  end
    2.92  
    2.93 @@ -219,7 +219,7 @@
    2.94  class idom = comm_ring_1 + no_zero_divisors
    2.95  begin
    2.96  
    2.97 -subclass ring_1_no_zero_divisors by unfold_locales
    2.98 +subclass ring_1_no_zero_divisors by intro_locales
    2.99  
   2.100  end
   2.101  
   2.102 @@ -261,7 +261,7 @@
   2.103    thus "a * inverse a = 1" by (simp only: mult_commute)
   2.104  qed
   2.105  
   2.106 -subclass idom by unfold_locales
   2.107 +subclass idom by intro_locales
   2.108  
   2.109  lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
   2.110  proof
   2.111 @@ -331,8 +331,8 @@
   2.112    + semiring + comm_monoid_add + cancel_ab_semigroup_add
   2.113  begin
   2.114  
   2.115 -subclass semiring_0_cancel by unfold_locales
   2.116 -subclass pordered_semiring by unfold_locales
   2.117 +subclass semiring_0_cancel by intro_locales
   2.118 +subclass pordered_semiring by intro_locales
   2.119  
   2.120  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   2.121    by (drule mult_left_mono [of zero b], auto)
   2.122 @@ -351,9 +351,9 @@
   2.123  class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   2.124  begin
   2.125  
   2.126 -subclass pordered_cancel_semiring by unfold_locales
   2.127 -
   2.128 -subclass pordered_comm_monoid_add by unfold_locales
   2.129 +subclass pordered_cancel_semiring by intro_locales
   2.130 +
   2.131 +subclass pordered_comm_monoid_add by intro_locales
   2.132  
   2.133  lemma mult_left_less_imp_less:
   2.134    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   2.135 @@ -370,7 +370,7 @@
   2.136    assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   2.137  begin
   2.138  
   2.139 -subclass semiring_0_cancel by unfold_locales
   2.140 +subclass semiring_0_cancel by intro_locales
   2.141  
   2.142  subclass ordered_semiring
   2.143  proof unfold_locales
   2.144 @@ -443,8 +443,8 @@
   2.145    + pordered_ab_semigroup_add + mult_mono1
   2.146  begin
   2.147  
   2.148 -subclass pordered_comm_semiring by unfold_locales
   2.149 -subclass pordered_cancel_semiring by unfold_locales
   2.150 +subclass pordered_comm_semiring by intro_locales
   2.151 +subclass pordered_cancel_semiring by intro_locales
   2.152  
   2.153  end
   2.154  
   2.155 @@ -474,7 +474,7 @@
   2.156  class pordered_ring = ring + pordered_cancel_semiring 
   2.157  begin
   2.158  
   2.159 -subclass pordered_ab_group_add by unfold_locales
   2.160 +subclass pordered_ab_group_add by intro_locales
   2.161  
   2.162  lemmas ring_simps = ring_simps group_simps
   2.163  
   2.164 @@ -526,7 +526,7 @@
   2.165    + ordered_ab_group_add + abs_if
   2.166  begin
   2.167  
   2.168 -subclass pordered_ring by unfold_locales
   2.169 +subclass pordered_ring by intro_locales
   2.170  
   2.171  subclass pordered_ab_group_add_abs
   2.172  proof unfold_locales
   2.173 @@ -547,7 +547,7 @@
   2.174    + ordered_ab_group_add + abs_if
   2.175  begin
   2.176  
   2.177 -subclass ordered_ring by unfold_locales
   2.178 +subclass ordered_ring by intro_locales
   2.179  
   2.180  lemma mult_strict_left_mono_neg:
   2.181    "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   2.182 @@ -614,8 +614,8 @@
   2.183  class pordered_comm_ring = comm_ring + pordered_comm_semiring
   2.184  begin
   2.185  
   2.186 -subclass pordered_ring by unfold_locales
   2.187 -subclass pordered_cancel_comm_semiring by unfold_locales
   2.188 +subclass pordered_ring by intro_locales
   2.189 +subclass pordered_cancel_comm_semiring by intro_locales
   2.190  
   2.191  end
   2.192  
   2.193 @@ -2017,8 +2017,8 @@
   2.194  class lordered_ring = pordered_ring + lordered_ab_group_add_abs
   2.195  begin
   2.196  
   2.197 -subclass lordered_ab_group_add_meet by unfold_locales
   2.198 -subclass lordered_ab_group_add_join by unfold_locales
   2.199 +subclass lordered_ab_group_add_meet by intro_locales
   2.200 +subclass lordered_ab_group_add_join by intro_locales
   2.201  
   2.202  end
   2.203