# HG changeset patch # User wenzelm # Date 1369601868 -7200 # Node ID 3c18725d576af76358c40446034ea7f976d1fd8e # Parent f5773a46cf058afd700bb9cf761820b1979bd477# Parent 72e83c82c1d487786951e4ae3655290fddaa37f3 merged diff -r 72e83c82c1d4 -r 3c18725d576a src/HOL/Lattices.thy --- 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 \ b \ a \ b \ a \ b" @@ -79,9 +77,6 @@ then show "a \ c" by (rule orderI) qed -context semilattice_order -begin - lemma cobounded1 [simp]: "a * b \ 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 \ b) \ c = a \ (b \ c)" @@ -266,26 +267,9 @@ by (rule antisym) auto qed -sublocale semilattice_sup < sup!: semilattice sup -proof - fix a b c - show "(a \ b) \ c = a \ (b \ c)" - by (rule antisym) (auto intro: le_supI1 le_supI2) - show "a \ b = b \ a" - by (rule antisym) auto - show "a \ 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 \ y) \ z = x \ (y \ z)" by (fact inf.assoc) @@ -317,6 +301,20 @@ context semilattice_sup begin +sublocale sup!: semilattice sup +proof + fix a b c + show "(a \ b) \ c = a \ (b \ c)" + by (rule antisym) (auto intro: le_supI1 le_supI2) + show "a \ b = b \ a" + by (rule antisym) auto + show "a \ 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 \ y) \ z = x \ (y \ 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 diff -r 72e83c82c1d4 -r 3c18725d576a src/Pure/Isar/expression.ML --- 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 diff -r 72e83c82c1d4 -r 3c18725d576a src/Pure/Isar/generic_target.ML --- 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 **) diff -r 72e83c82c1d4 -r 3c18725d576a src/Pure/Isar/local_theory.ML --- 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 **)