author haftmann Fri, 02 Nov 2007 18:52:58 +0100 changeset 25267 1f745c599b5c parent 25266 37aa898e0523 child 25268 58146cb7bf44
proper reinitialisation after subclass
 src/HOL/OrderedGroup.thy file | annotate | diff | comparison | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | comparison | revisions src/Pure/Isar/subclass.ML file | annotate | diff | comparison | revisions
```--- 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 @@

assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+begin

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
+
begin

@@ -219,11 +222,12 @@
assumes ab_left_minus: "- a + a = 0"
assumes ab_diff_minus: "a - b = a + (- b)"
+begin

by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)

proof unfold_locales
fix a b c :: 'a
assume "a + b = a + c"
@@ -232,9 +236,6 @@
then show "b = c" by simp
qed

-begin
-
"- a + b = b - a"
@@ -409,11 +410,6 @@
thus "a \<le> b" by simp
qed

-end
-
-begin
-
lemma max_diff_distrib_left:
shows "max x y - z = max (x - z) (y - z)"
@@ -555,11 +551,12 @@

+begin

by unfold_locales

proof unfold_locales
fix a b c :: 'a
assume le: "c + a <= c + b"
@@ -578,12 +575,17 @@
qed
qed

+end
+
+begin

by unfold_locales

+end
+
-- {* FIXME localize the following *}

@@ -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
-

lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"```
```--- 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
+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
+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
+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

-
-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 @@
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
-
-class pordered_cancel_comm_semiring = comm_semiring_0_cancel
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
+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

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*)```
```--- 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;```