--- a/src/HOL/Lattices.thy Sun May 26 22:47:00 2013 +0200
+++ b/src/HOL/Lattices.thy Sun May 26 22:57:48 2013 +0200
@@ -49,9 +49,7 @@
obtains "a = a * b"
using assms by (unfold order_iff)
-end
-
-sublocale semilattice_order < ordering less_eq less
+sublocale ordering less_eq less
proof
fix a b
show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
@@ -79,9 +77,6 @@
then show "a \<preceq> c" by (rule orderI)
qed
-context semilattice_order
-begin
-
lemma cobounded1 [simp]:
"a * b \<preceq> a"
by (simp add: order_iff commute)
@@ -132,10 +127,13 @@
end
locale semilattice_neutr_order = semilattice_neutr + semilattice_order
+begin
-sublocale semilattice_neutr_order < ordering_top less_eq less 1
+sublocale ordering_top less_eq less 1
by default (simp add: order_iff)
+end
+
notation times (infixl "*" 70)
notation Groups.one ("1")
@@ -255,7 +253,10 @@
subsubsection {* Equational laws *}
-sublocale semilattice_inf < inf!: semilattice inf
+context semilattice_inf
+begin
+
+sublocale inf!: semilattice inf
proof
fix a b c
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
@@ -266,26 +267,9 @@
by (rule antisym) auto
qed
-sublocale semilattice_sup < sup!: semilattice sup
-proof
- fix a b c
- show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
- by (rule antisym) (auto intro: le_supI1 le_supI2)
- show "a \<squnion> b = b \<squnion> a"
- by (rule antisym) auto
- show "a \<squnion> a = a"
- by (rule antisym) auto
-qed
-
-sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
+sublocale inf!: semilattice_order inf less_eq less
by default (auto simp add: le_iff_inf less_le)
-sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
- by default (auto simp add: le_iff_sup sup.commute less_le)
-
-context semilattice_inf
-begin
-
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
by (fact inf.assoc)
@@ -317,6 +301,20 @@
context semilattice_sup
begin
+sublocale sup!: semilattice sup
+proof
+ fix a b c
+ show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
+ by (rule antisym) (auto intro: le_supI1 le_supI2)
+ show "a \<squnion> b = b \<squnion> a"
+ by (rule antisym) auto
+ show "a \<squnion> a = a"
+ by (rule antisym) auto
+qed
+
+sublocale sup!: semilattice_order sup greater_eq greater
+ by default (auto simp add: le_iff_sup sup.commute less_le)
+
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
by (fact sup.assoc)
@@ -469,8 +467,9 @@
subsection {* Bounded lattices and boolean algebras *}
class bounded_semilattice_inf_top = semilattice_inf + top
+begin
-sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+sublocale inf_top!: semilattice_neutr inf top
+ inf_top!: semilattice_neutr_order inf top less_eq less
proof
fix x
@@ -478,9 +477,12 @@
by (rule inf_absorb1) simp
qed
-class bounded_semilattice_sup_bot = semilattice_sup + bot
+end
-sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+class bounded_semilattice_sup_bot = semilattice_sup + bot
+begin
+
+sublocale sup_bot!: semilattice_neutr sup bot
+ sup_bot!: semilattice_neutr_order sup bot greater_eq greater
proof
fix x
@@ -488,6 +490,8 @@
by (rule sup_absorb1) simp
qed
+end
+
class bounded_lattice_bot = lattice + bot
begin
--- a/src/Pure/Isar/expression.ML Sun May 26 22:47:00 2013 +0200
+++ b/src/Pure/Isar/expression.ML Sun May 26 22:57:48 2013 +0200
@@ -882,7 +882,7 @@
then
lthy
|> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
- Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
+ Local_Theory.notes_kind Generic_Target.theory_registration expression raw_eqns
else
lthy
|> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
@@ -895,7 +895,7 @@
in
lthy
|> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
- Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
+ Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns
end;
fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
@@ -915,8 +915,8 @@
let
val _ = Local_Theory.assert_bottom true lthy;
val target = Named_Target.the_name lthy;
- val subscribe = if target = "" then Local_Theory.add_registration
- else Local_Theory.add_dependency target;
+ val subscribe = if target = "" then Generic_Target.theory_registration
+ else Generic_Target.locale_dependency target;
in
lthy
|> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
--- a/src/Pure/Isar/generic_target.ML Sun May 26 22:47:00 2013 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun May 26 22:57:48 2013 +0200
@@ -41,6 +41,10 @@
val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
local_theory -> local_theory
val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
+ val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -271,6 +275,16 @@
in generic_const same_shape prmode ((b', mx), rhs') end);
+(* registrations and dependencies *)
+
+val theory_registration =
+ Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
+
+fun locale_dependency locale dep_morph mixin export =
+ (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
+ #> Local_Theory.activate_nonbrittle dep_morph mixin export;
+
+
(** primitive theory operations **)
--- a/src/Pure/Isar/local_theory.ML Sun May 26 22:47:00 2013 +0200
+++ b/src/Pure/Isar/local_theory.ML Sun May 26 22:57:48 2013 +0200
@@ -58,9 +58,7 @@
val const_alias: binding -> string -> local_theory -> local_theory
val activate: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
- val add_registration: string * morphism -> (morphism * bool) option -> morphism ->
- local_theory -> local_theory
- val add_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+ val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
val init: Name_Space.naming -> operations -> Proof.context -> local_theory
val exit: local_theory -> Proof.context
@@ -308,19 +306,13 @@
(* activation of locale fragments *)
-fun activate_surface dep_morph mixin export =
+fun activate_nonbrittle dep_morph mixin export =
map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
(naming, operations, after_close, brittle,
(Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
fun activate dep_morph mixin export =
- mark_brittle #> activate_surface dep_morph mixin export;
-
-val add_registration = raw_theory o Context.theory_map ooo Locale.add_registration;
-
-fun add_dependency locale dep_morph mixin export =
- (raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
- #> activate_surface dep_morph mixin export;
+ mark_brittle #> activate_nonbrittle dep_morph mixin export;
(** init and exit **)