proper reinitialisation after subclass
authorhaftmann
Fri Nov 02 18:52:58 2007 +0100 (2007-11-02)
changeset 252671f745c599b5c
parent 25266 37aa898e0523
child 25268 58146cb7bf44
proper reinitialisation after subclass
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
src/Pure/Isar/subclass.ML
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Nov 02 18:52:57 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Nov 02 18:52:58 2007 +0100
     1.3 @@ -90,8 +90,9 @@
     1.4  
     1.5  class cancel_ab_semigroup_add = ab_semigroup_add +
     1.6    assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
     1.7 +begin
     1.8  
     1.9 -subclass (in cancel_ab_semigroup_add) cancel_semigroup_add
    1.10 +subclass cancel_semigroup_add
    1.11  proof unfold_locales
    1.12    fix a b c :: 'a
    1.13    assume "a + b = a + c" 
    1.14 @@ -103,6 +104,8 @@
    1.15    then show "b = c" by (rule add_imp_eq)
    1.16  qed
    1.17  
    1.18 +end
    1.19 +
    1.20  context cancel_ab_semigroup_add
    1.21  begin
    1.22  
    1.23 @@ -219,11 +222,12 @@
    1.24  class ab_group_add = minus + comm_monoid_add +
    1.25    assumes ab_left_minus: "- a + a = 0"
    1.26    assumes ab_diff_minus: "a - b = a + (- b)"
    1.27 +begin
    1.28  
    1.29 -subclass (in ab_group_add) group_add
    1.30 +subclass group_add
    1.31    by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
    1.32  
    1.33 -subclass (in ab_group_add) cancel_ab_semigroup_add
    1.34 +subclass cancel_ab_semigroup_add
    1.35  proof unfold_locales
    1.36    fix a b c :: 'a
    1.37    assume "a + b = a + c"
    1.38 @@ -232,9 +236,6 @@
    1.39    then show "b = c" by simp
    1.40  qed
    1.41  
    1.42 -context ab_group_add
    1.43 -begin
    1.44 -
    1.45  lemma uminus_add_conv_diff:
    1.46    "- a + b = b - a"
    1.47    by (simp add:diff_minus add_commute)
    1.48 @@ -409,11 +410,6 @@
    1.49    thus "a \<le> b" by simp
    1.50  qed
    1.51  
    1.52 -end
    1.53 -
    1.54 -context pordered_ab_group_add
    1.55 -begin
    1.56 -
    1.57  lemma max_diff_distrib_left:
    1.58    shows "max x y - z = max (x - z) (y - z)"
    1.59    by (simp add: diff_minus, rule max_add_distrib_left) 
    1.60 @@ -555,11 +551,12 @@
    1.61  
    1.62  class ordered_cancel_ab_semigroup_add =
    1.63    linorder + pordered_cancel_ab_semigroup_add
    1.64 +begin
    1.65  
    1.66 -subclass (in ordered_cancel_ab_semigroup_add) ordered_ab_semigroup_add
    1.67 +subclass ordered_ab_semigroup_add
    1.68    by unfold_locales
    1.69  
    1.70 -subclass (in ordered_cancel_ab_semigroup_add) pordered_ab_semigroup_add_imp_le
    1.71 +subclass pordered_ab_semigroup_add_imp_le
    1.72  proof unfold_locales
    1.73    fix a b c :: 'a
    1.74    assume le: "c + a <= c + b"  
    1.75 @@ -578,12 +575,17 @@
    1.76    qed
    1.77  qed
    1.78  
    1.79 +end
    1.80 +
    1.81  class ordered_ab_group_add =
    1.82    linorder + pordered_ab_group_add
    1.83 +begin
    1.84  
    1.85 -subclass (in ordered_ab_group_add) ordered_cancel_ab_semigroup_add 
    1.86 +subclass ordered_cancel_ab_semigroup_add 
    1.87    by unfold_locales
    1.88  
    1.89 +end
    1.90 +
    1.91  -- {* FIXME localize the following *}
    1.92  
    1.93  lemma add_increasing:
    1.94 @@ -728,11 +730,6 @@
    1.95  subclass lordered_ab_group_meet by unfold_locales
    1.96  subclass lordered_ab_group_join by unfold_locales
    1.97  
    1.98 -end
    1.99 -
   1.100 -context lordered_ab_group
   1.101 -begin
   1.102 -
   1.103  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   1.104  
   1.105  lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
     2.1 --- a/src/HOL/Ring_and_Field.thy	Fri Nov 02 18:52:57 2007 +0100
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Nov 02 18:52:58 2007 +0100
     2.3 @@ -109,24 +109,28 @@
     2.4  
     2.5  class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
     2.6    + cancel_ab_semigroup_add + monoid_mult
     2.7 +begin
     2.8  
     2.9 -subclass (in semiring_1_cancel) semiring_0_cancel by unfold_locales
    2.10 +subclass semiring_0_cancel by unfold_locales
    2.11  
    2.12 -subclass (in semiring_1_cancel) semiring_1 by unfold_locales
    2.13 +subclass semiring_1 by unfold_locales
    2.14 +
    2.15 +end
    2.16  
    2.17  class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
    2.18    + zero_neq_one + cancel_ab_semigroup_add
    2.19 +begin
    2.20  
    2.21 -subclass (in comm_semiring_1_cancel) semiring_1_cancel by unfold_locales
    2.22 -subclass (in comm_semiring_1_cancel) comm_semiring_0_cancel by unfold_locales
    2.23 -subclass (in comm_semiring_1_cancel) comm_semiring_1 by unfold_locales
    2.24 +subclass semiring_1_cancel by unfold_locales
    2.25 +subclass comm_semiring_0_cancel by unfold_locales
    2.26 +subclass comm_semiring_1 by unfold_locales
    2.27 +
    2.28 +end
    2.29  
    2.30  class ring = semiring + ab_group_add
    2.31 -
    2.32 -subclass (in ring) semiring_0_cancel by unfold_locales
    2.33 +begin
    2.34  
    2.35 -context ring
    2.36 -begin
    2.37 +subclass semiring_0_cancel by unfold_locales
    2.38  
    2.39  text {* Distribution rules *}
    2.40  
    2.41 @@ -173,19 +177,28 @@
    2.42    right_distrib left_distrib left_diff_distrib right_diff_distrib
    2.43  
    2.44  class comm_ring = comm_semiring + ab_group_add
    2.45 +begin
    2.46  
    2.47 -subclass (in comm_ring) ring by unfold_locales
    2.48 -subclass (in comm_ring) comm_semiring_0 by unfold_locales
    2.49 +subclass ring by unfold_locales
    2.50 +subclass comm_semiring_0 by unfold_locales
    2.51 +
    2.52 +end
    2.53  
    2.54  class ring_1 = ring + zero_neq_one + monoid_mult
    2.55 +begin
    2.56  
    2.57 -subclass (in ring_1) semiring_1_cancel by unfold_locales
    2.58 +subclass semiring_1_cancel by unfold_locales
    2.59 +
    2.60 +end
    2.61  
    2.62  class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
    2.63    (*previously ring*)
    2.64 +begin
    2.65  
    2.66 -subclass (in comm_ring_1) ring_1 by unfold_locales
    2.67 -subclass (in comm_ring_1) comm_semiring_1_cancel by unfold_locales
    2.68 +subclass ring_1 by unfold_locales
    2.69 +subclass comm_semiring_1_cancel by unfold_locales
    2.70 +
    2.71 +end
    2.72  
    2.73  class ring_no_zero_divisors = ring + no_zero_divisors
    2.74  begin
    2.75 @@ -238,8 +251,9 @@
    2.76  class field = comm_ring_1 + inverse +
    2.77    assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    2.78    assumes divide_inverse: "a / b = a * inverse b"
    2.79 +begin
    2.80  
    2.81 -subclass (in field) division_ring
    2.82 +subclass division_ring
    2.83  proof unfold_locales
    2.84    fix a :: 'a
    2.85    assume "a \<noteq> 0"
    2.86 @@ -247,10 +261,7 @@
    2.87    thus "a * inverse a = 1" by (simp only: mult_commute)
    2.88  qed
    2.89  
    2.90 -subclass (in field) idom by unfold_locales
    2.91 -
    2.92 -context field
    2.93 -begin
    2.94 +subclass idom by unfold_locales
    2.95  
    2.96  lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
    2.97  proof
    2.98 @@ -318,12 +329,10 @@
    2.99  
   2.100  class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   2.101    + semiring + comm_monoid_add + cancel_ab_semigroup_add
   2.102 +begin
   2.103  
   2.104 -subclass (in pordered_cancel_semiring) semiring_0_cancel by unfold_locales
   2.105 -subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales
   2.106 -
   2.107 -context pordered_cancel_semiring
   2.108 -begin
   2.109 +subclass semiring_0_cancel by unfold_locales
   2.110 +subclass pordered_semiring by unfold_locales
   2.111  
   2.112  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   2.113    by (drule mult_left_mono [of zero b], auto)
   2.114 @@ -340,11 +349,9 @@
   2.115  end
   2.116  
   2.117  class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   2.118 -
   2.119 -subclass (in ordered_semiring) pordered_cancel_semiring by unfold_locales
   2.120 +begin
   2.121  
   2.122 -context ordered_semiring
   2.123 -begin
   2.124 +subclass pordered_cancel_semiring by unfold_locales
   2.125  
   2.126  lemma mult_left_less_imp_less:
   2.127    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   2.128 @@ -359,10 +366,11 @@
   2.129  class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   2.130    assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   2.131    assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   2.132 +begin
   2.133  
   2.134 -subclass (in ordered_semiring_strict) semiring_0_cancel by unfold_locales
   2.135 +subclass semiring_0_cancel by unfold_locales
   2.136  
   2.137 -subclass (in ordered_semiring_strict) ordered_semiring
   2.138 +subclass ordered_semiring
   2.139  proof unfold_locales
   2.140    fix a b c :: 'a
   2.141    assume A: "a \<le> b" "0 \<le> c"
   2.142 @@ -374,9 +382,6 @@
   2.143      using mult_strict_right_mono by (cases "c = 0") auto
   2.144  qed
   2.145  
   2.146 -context ordered_semiring_strict
   2.147 -begin
   2.148 -
   2.149  lemma mult_left_le_imp_le:
   2.150    "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   2.151    by (force simp add: mult_strict_left_mono _not_less [symmetric])
   2.152 @@ -420,19 +425,9 @@
   2.153  
   2.154  class pordered_comm_semiring = comm_semiring_0
   2.155    + pordered_ab_semigroup_add + mult_mono1
   2.156 -
   2.157 -class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   2.158 -  + pordered_ab_semigroup_add + mult_mono1
   2.159  begin
   2.160  
   2.161 -subclass pordered_comm_semiring by unfold_locales
   2.162 -
   2.163 -end
   2.164 -
   2.165 -class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   2.166 -  assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   2.167 -
   2.168 -subclass (in pordered_comm_semiring) pordered_semiring
   2.169 +subclass pordered_semiring
   2.170  proof unfold_locales
   2.171    fix a b c :: 'a
   2.172    assume "a \<le> b" "0 \<le> c"
   2.173 @@ -440,10 +435,22 @@
   2.174    thus "a * c \<le> b * c" by (simp only: mult_commute)
   2.175  qed
   2.176  
   2.177 -subclass (in pordered_cancel_comm_semiring) pordered_cancel_semiring
   2.178 -  by unfold_locales
   2.179 +end
   2.180 +
   2.181 +class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   2.182 +  + pordered_ab_semigroup_add + mult_mono1
   2.183 +begin
   2.184  
   2.185 -subclass (in ordered_comm_semiring_strict) ordered_semiring_strict
   2.186 +subclass pordered_comm_semiring by unfold_locales
   2.187 +subclass pordered_cancel_semiring by unfold_locales
   2.188 +
   2.189 +end
   2.190 +
   2.191 +class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   2.192 +  assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   2.193 +begin
   2.194 +
   2.195 +subclass ordered_semiring_strict
   2.196  proof unfold_locales
   2.197    fix a b c :: 'a
   2.198    assume "a < b" "0 < c"
   2.199 @@ -451,7 +458,7 @@
   2.200    thus "a * c < b * c" by (simp only: mult_commute)
   2.201  qed
   2.202  
   2.203 -subclass (in ordered_comm_semiring_strict) pordered_cancel_comm_semiring
   2.204 +subclass pordered_cancel_comm_semiring
   2.205  proof unfold_locales
   2.206    fix a b c :: 'a
   2.207    assume "a \<le> b" "0 \<le> c"
   2.208 @@ -460,12 +467,12 @@
   2.209      using mult_strict_mono by (cases "c = 0") auto
   2.210  qed
   2.211  
   2.212 -class pordered_ring = ring + pordered_cancel_semiring 
   2.213 +end
   2.214  
   2.215 -subclass (in pordered_ring) pordered_ab_group_add by unfold_locales
   2.216 +class pordered_ring = ring + pordered_cancel_semiring 
   2.217 +begin
   2.218  
   2.219 -context pordered_ring
   2.220 -begin
   2.221 +subclass pordered_ab_group_add by unfold_locales
   2.222  
   2.223  lemmas ring_simps = ring_simps group_simps
   2.224  
   2.225 @@ -508,9 +515,12 @@
   2.226  end
   2.227  
   2.228  class lordered_ring = pordered_ring + lordered_ab_group_abs
   2.229 +begin
   2.230  
   2.231 -subclass (in lordered_ring) lordered_ab_group_meet by unfold_locales
   2.232 -subclass (in lordered_ring) lordered_ab_group_join by unfold_locales
   2.233 +subclass lordered_ab_group_meet by unfold_locales
   2.234 +subclass lordered_ab_group_join by unfold_locales
   2.235 +
   2.236 +end
   2.237  
   2.238  class abs_if = minus + ord + zero + abs +
   2.239    assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
   2.240 @@ -606,10 +616,12 @@
   2.241  
   2.242  
   2.243  class pordered_comm_ring = comm_ring + pordered_comm_semiring
   2.244 +begin
   2.245  
   2.246 -subclass (in pordered_comm_ring) pordered_ring by unfold_locales
   2.247 +subclass pordered_ring by unfold_locales
   2.248 +subclass pordered_cancel_comm_semiring by unfold_locales
   2.249  
   2.250 -subclass (in pordered_comm_ring) pordered_cancel_comm_semiring by unfold_locales
   2.251 +end
   2.252  
   2.253  class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   2.254    (*previously ordered_semiring*)
     3.1 --- a/src/Pure/Isar/subclass.ML	Fri Nov 02 18:52:57 2007 +0100
     3.2 +++ b/src/Pure/Isar/subclass.ML	Fri Nov 02 18:52:58 2007 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4        |> map (ObjectLogic.ensure_propT thy);
     3.5      fun after_qed thms =
     3.6        LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt)
     3.7 -      (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*);
     3.8 +      #> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of (LocalTheory.target_of lthy)));
     3.9    in
    3.10      do_proof after_qed sublocale_prop lthy
    3.11    end;