# HG changeset patch
# User haftmann
# Date 1194025978 -3600
# Node ID 1f745c599b5cc1046185977cab1ac569a2f1631a
# Parent  37aa898e05230180bf427c44095a7e8af8dde69c
proper reinitialisation after subclass

diff -r 37aa898e0523 -r 1f745c599b5c src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Nov 02 18:52:57 2007 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Nov 02 18:52:58 2007 +0100
@@ -90,8 +90,9 @@
 
 class cancel_ab_semigroup_add = ab_semigroup_add +
   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+begin
 
-subclass (in cancel_ab_semigroup_add) cancel_semigroup_add
+subclass cancel_semigroup_add
 proof unfold_locales
   fix a b c :: 'a
   assume "a + b = a + c" 
@@ -103,6 +104,8 @@
   then show "b = c" by (rule add_imp_eq)
 qed
 
+end
+
 context cancel_ab_semigroup_add
 begin
 
@@ -219,11 +222,12 @@
 class ab_group_add = minus + comm_monoid_add +
   assumes ab_left_minus: "- a + a = 0"
   assumes ab_diff_minus: "a - b = a + (- b)"
+begin
 
-subclass (in ab_group_add) group_add
+subclass group_add
   by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
 
-subclass (in ab_group_add) cancel_ab_semigroup_add
+subclass cancel_ab_semigroup_add
 proof unfold_locales
   fix a b c :: 'a
   assume "a + b = a + c"
@@ -232,9 +236,6 @@
   then show "b = c" by simp
 qed
 
-context ab_group_add
-begin
-
 lemma uminus_add_conv_diff:
   "- a + b = b - a"
   by (simp add:diff_minus add_commute)
@@ -409,11 +410,6 @@
   thus "a \<le> b" by simp
 qed
 
-end
-
-context pordered_ab_group_add
-begin
-
 lemma max_diff_distrib_left:
   shows "max x y - z = max (x - z) (y - z)"
   by (simp add: diff_minus, rule max_add_distrib_left) 
@@ -555,11 +551,12 @@
 
 class ordered_cancel_ab_semigroup_add =
   linorder + pordered_cancel_ab_semigroup_add
+begin
 
-subclass (in ordered_cancel_ab_semigroup_add) ordered_ab_semigroup_add
+subclass ordered_ab_semigroup_add
   by unfold_locales
 
-subclass (in ordered_cancel_ab_semigroup_add) pordered_ab_semigroup_add_imp_le
+subclass pordered_ab_semigroup_add_imp_le
 proof unfold_locales
   fix a b c :: 'a
   assume le: "c + a <= c + b"  
@@ -578,12 +575,17 @@
   qed
 qed
 
+end
+
 class ordered_ab_group_add =
   linorder + pordered_ab_group_add
+begin
 
-subclass (in ordered_ab_group_add) ordered_cancel_ab_semigroup_add 
+subclass ordered_cancel_ab_semigroup_add 
   by unfold_locales
 
+end
+
 -- {* FIXME localize the following *}
 
 lemma add_increasing:
@@ -728,11 +730,6 @@
 subclass lordered_ab_group_meet by unfold_locales
 subclass lordered_ab_group_join by unfold_locales
 
-end
-
-context lordered_ab_group
-begin
-
 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
 
 lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
diff -r 37aa898e0523 -r 1f745c599b5c src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Nov 02 18:52:57 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Nov 02 18:52:58 2007 +0100
@@ -109,24 +109,28 @@
 
 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
   + cancel_ab_semigroup_add + monoid_mult
+begin
 
-subclass (in semiring_1_cancel) semiring_0_cancel by unfold_locales
+subclass semiring_0_cancel by unfold_locales
 
-subclass (in semiring_1_cancel) semiring_1 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
+begin
 
-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
+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
+begin
 
-context ring
-begin
+subclass semiring_0_cancel by unfold_locales
 
 text {* Distribution rules *}
 
@@ -173,19 +177,28 @@
   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
+begin
 
-subclass (in comm_ring) ring by unfold_locales
-subclass (in comm_ring) comm_semiring_0 by unfold_locales
+subclass ring by unfold_locales
+subclass comm_semiring_0 by unfold_locales
+
+end
 
 class ring_1 = ring + zero_neq_one + monoid_mult
+begin
 
-subclass (in ring_1) semiring_1_cancel by unfold_locales
+subclass semiring_1_cancel by unfold_locales
+
+end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   (*previously ring*)
+begin
 
-subclass (in comm_ring_1) ring_1 by unfold_locales
-subclass (in comm_ring_1) comm_semiring_1_cancel by unfold_locales
+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
@@ -238,8 +251,9 @@
 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"
+begin
 
-subclass (in field) division_ring
+subclass division_ring
 proof unfold_locales
   fix a :: 'a
   assume "a \<noteq> 0"
@@ -247,10 +261,7 @@
   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
@@ -318,12 +329,10 @@
 
 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   + semiring + comm_monoid_add + cancel_ab_semigroup_add
+begin
 
-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
+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)
@@ -340,11 +349,9 @@
 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
+begin
 
-context ordered_semiring
-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"
@@ -359,10 +366,11 @@
 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 (in ordered_semiring_strict) semiring_0_cancel by unfold_locales
+subclass semiring_0_cancel by unfold_locales
 
-subclass (in ordered_semiring_strict) ordered_semiring
+subclass ordered_semiring
 proof unfold_locales
   fix a b c :: 'a
   assume A: "a \<le> b" "0 \<le> c"
@@ -374,9 +382,6 @@
     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])
@@ -420,19 +425,9 @@
 
 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
+subclass pordered_semiring
 proof unfold_locales
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
@@ -440,10 +435,22 @@
   thus "a * c \<le> b * c" by (simp only: mult_commute)
 qed
 
-subclass (in pordered_cancel_comm_semiring) pordered_cancel_semiring
-  by unfold_locales
+end
+
+class pordered_cancel_comm_semiring = comm_semiring_0_cancel
+  + pordered_ab_semigroup_add + mult_mono1
+begin
 
-subclass (in ordered_comm_semiring_strict) ordered_semiring_strict
+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"
@@ -451,7 +458,7 @@
   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"
@@ -460,12 +467,12 @@
     using mult_strict_mono by (cases "c = 0") auto
 qed
 
-class pordered_ring = ring + pordered_cancel_semiring 
+end
 
-subclass (in pordered_ring) pordered_ab_group_add by unfold_locales
+class pordered_ring = ring + pordered_cancel_semiring 
+begin
 
-context pordered_ring
-begin
+subclass pordered_ab_group_add by unfold_locales
 
 lemmas ring_simps = ring_simps group_simps
 
@@ -508,9 +515,12 @@
 end
 
 class lordered_ring = pordered_ring + lordered_ab_group_abs
+begin
 
-subclass (in lordered_ring) lordered_ab_group_meet by unfold_locales
-subclass (in lordered_ring) lordered_ab_group_join by unfold_locales
+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)"
@@ -606,10 +616,12 @@
 
 
 class pordered_comm_ring = comm_ring + pordered_comm_semiring
+begin
 
-subclass (in pordered_comm_ring) pordered_ring by unfold_locales
+subclass pordered_ring by unfold_locales
+subclass pordered_cancel_comm_semiring by unfold_locales
 
-subclass (in pordered_comm_ring) pordered_cancel_comm_semiring by unfold_locales
+end
 
 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   (*previously ordered_semiring*)
diff -r 37aa898e0523 -r 1f745c599b5c src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Fri Nov 02 18:52:57 2007 +0100
+++ b/src/Pure/Isar/subclass.ML	Fri Nov 02 18:52:58 2007 +0100
@@ -38,7 +38,7 @@
       |> map (ObjectLogic.ensure_propT thy);
     fun after_qed thms =
       LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt)
-      (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*);
+      #> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of (LocalTheory.target_of lthy)));
   in
     do_proof after_qed sublocale_prop lthy
   end;