--- a/doc-src/Locales/Locales/Examples3.thy Sat Sep 19 18:43:11 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Tue Sep 29 22:15:54 2009 +0200
@@ -14,7 +14,7 @@
interpretation. The third revision of the example illustrates this. *}
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where nat_less_eq: "partial_order.less op \<le> (x::nat) y = (x < y)"
+ where "partial_order.less op \<le> (x::nat) y = (x < y)"
proof -
show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
by unfold_locales auto
@@ -44,11 +44,10 @@
elaborate interpretation proof. *}
interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
- and nat_meet_eq: "lattice.meet op \<le> (x::nat) y = min x y"
- and nat_join_eq: "lattice.join op \<le> (x::nat) y = max x y"
+ where "lattice.meet op \<le> (x::nat) y = min x y"
+ and "lattice.join op \<le> (x::nat) y = max x y"
proof -
- show lattice: "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+ show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
txt {* We have already shown that this is a partial order, *}
apply unfold_locales
txt {* hence only the lattice axioms remain to be shown: @{subgoals
@@ -57,13 +56,9 @@
txt {* the goals become @{subgoals [display]} which can be solved
by Presburger arithmetic. *}
by arith+
- txt {* For the first of the equations, we refer to the theorem
- shown in the previous interpretation. *}
- show "partial_order.less op \<le> (x::nat) y = (x < y)"
- by (rule nat_less_eq)
- txt {* In order to show the remaining equations, we put ourselves in a
+ txt {* In order to show the equations, we put ourselves in a
situation where the lattice theorems can be used in a convenient way. *}
- from lattice interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
+ then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
show "lattice.meet op \<le> (x::nat) y = min x y"
by (bestsimp simp: nat.meet_def nat.is_inf_def)
show "lattice.join op \<le> (x::nat) y = max x y"
@@ -73,25 +68,7 @@
text {* Next follows that @{text \<le>} is a total order. *}
interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
- and "lattice.meet op \<le> (x::nat) y = min x y"
- and "lattice.join op \<le> (x::nat) y = max x y"
-proof -
- show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- by unfold_locales arith
-qed (rule nat_less_eq nat_meet_eq nat_join_eq)+
-
-text {* Since the locale hierarchy reflects that total
- orders are distributive lattices, an explicit interpretation of
- distributive lattices for the order relation on natural numbers is
- only necessary for mapping the definitions to the right operators on
- @{typ nat}. *}
-
-interpretation %visible nat: distrib_lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
- and "lattice.meet op \<le> (x::nat) y = min x y"
- and "lattice.join op \<le> (x::nat) y = max x y"
- by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+
+ by unfold_locales arith
text {* Theorems that are available in the theory at this point are shown in
Table~\ref{tab:nat-lattice}.
@@ -115,6 +92,29 @@
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
\label{tab:nat-lattice}
\end{table}
+
+ Note that since the locale hierarchy reflects that total orders are
+ distributive lattices, an explicit interpretation of distributive
+ lattices for the order relation on natural numbers is not neccessary.
+
+ Why not push this idea further and just give the last interpretation
+ as a single interpretation instead of the sequence of three? The
+ reasons for this are twofold:
+\begin{itemize}
+\item
+ Often it is easier to work in an incremental fashion, because later
+ interpretations require theorems provided by earlier
+ interpretations.
+\item
+ Assume that a definition is made in some locale $l_1$, and that $l_2$
+ imports $l_1$. Let an equation for the definition be
+ proved in an interpretation of $l_2$. The equation will be unfolded
+ in interpretations of theorems added to $l_2$ or below in the import
+ hierarchy, but not for theorems added above $l_2$.
+ Hence, an equation interpreting a definition should always be given in
+ an interpretation of the locale where the definition is made, not in
+ an interpretation of a locale further down the hierarchy.
+\end{itemize}
*}
@@ -125,8 +125,7 @@
incrementally. *}
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where nat_dvd_less_eq:
- "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+ where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
proof -
show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
by unfold_locales (auto simp: dvd_def)
@@ -142,8 +141,7 @@
x \<noteq> y"}. *}
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+ where nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
and nat_dvd_join_eq: "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
proof -
show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
@@ -155,8 +153,6 @@
apply (auto intro: lcm_least_nat)
done
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
- show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- by (rule nat_dvd_less_eq)
show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
apply (auto simp add: expand_fun_eq)
apply (unfold nat_dvd.meet_def)
@@ -198,18 +194,11 @@
interpretation %visible nat_dvd:
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- and "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
- and "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
-proof -
- show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
- apply unfold_locales
- txt {* @{subgoals [display]} *}
- apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
- txt {* @{subgoals [display]} *}
- apply (rule gcd_lcm_distr)
- done
-qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+
+ apply unfold_locales
+ txt {* @{subgoals [display]} *}
+ apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
+ txt {* @{subgoals [display]} *}
+ apply (rule gcd_lcm_distr) done
text {* Theorems that are available in the theory after these
--- a/src/Pure/Isar/locale.ML Sat Sep 19 18:43:11 2009 +0200
+++ b/src/Pure/Isar/locale.ML Tue Sep 29 22:15:54 2009 +0200
@@ -68,8 +68,8 @@
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Registrations and dependencies *)
- val add_registration: string * morphism -> morphism -> theory -> theory
- val amend_registration: morphism * bool -> string * morphism -> theory -> theory
+ val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
+ val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
val add_dependency: string -> string * morphism -> morphism -> theory -> theory
@@ -77,6 +77,7 @@
(* Diagnostic *)
val print_locales: theory -> unit
val print_locale: theory -> bool -> xstring -> unit
+ val print_registrations: theory -> string -> unit
end;
structure Locale: LOCALE =
@@ -179,6 +180,7 @@
(** Identifiers: activated locales in theory or proof context **)
fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+(* FIXME: this is ident_le, smaller term is more general *)
local
@@ -214,13 +216,13 @@
val roundup_bound = 120;
-fun add thy depth (name, morph) (deps, marked) =
+fun add thy depth export (name, morph) (deps, marked) =
if depth > roundup_bound
then error "Roundup bound exceeded (sublocale relation probably not terminating)."
else
let
val dependencies = dependencies_of thy name;
- val instance = instance_of thy name morph;
+ val instance = instance_of thy name (morph $> export);
in
if member (ident_eq thy) marked (name, instance)
then (deps, marked)
@@ -228,7 +230,7 @@
let
val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
val marked' = (name, instance) :: marked;
- val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
+ val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
in
((name, morph) :: deps' @ deps, marked'')
end
@@ -236,14 +238,17 @@
in
-fun roundup thy activate_dep (name, morph) (marked, input) =
+(* Note that while identifiers always have the external (exported) view, activate_dep is
+ is presented with the internal view. *)
+
+fun roundup thy activate_dep export (name, morph) (marked, input) =
let
(* Find all dependencies incuding new ones (which are dependencies enriching
existing registrations). *)
- val (dependencies, marked') = add thy 0 (name, morph) ([], []);
+ val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
(* Filter out fragments from marked; these won't be activated. *)
val dependencies' = filter_out (fn (name, morph) =>
- member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
+ member (ident_eq thy) marked (name, instance_of thy name (morph $> export))) dependencies;
in
(merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
end;
@@ -287,7 +292,7 @@
else I);
val activate = activate_notes activ_elem transfer thy;
in
- roundup thy activate (name, Morphism.identity) (marked, input')
+ roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
end;
@@ -296,13 +301,13 @@
fun activate_declarations dep = Context.proof_map (fn context =>
let
val thy = Context.theory_of context;
- in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end);
+ in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end);
fun activate_facts dep context =
let
val thy = Context.theory_of context;
val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
- in roundup thy activate dep (get_idents context, context) |-> put_idents end;
+ in roundup thy activate Morphism.identity dep (get_idents context, context) |-> put_idents end;
fun init name thy =
activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
@@ -357,20 +362,97 @@
fun all_registrations thy = Registrations.get thy
|-> (fn regs => fn mixins => map (reg_morph mixins) regs);
-fun collect_mixins thy (name, base_morph) = Registrations.get thy
- |>> filter (fn ((name', (morph', _)), _) => ident_eq thy
- ((name, instance_of thy name base_morph), (name', instance_of thy name' morph')))
- |-> (fn regs => fn mixins =>
- fold_rev (fn (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
- |> curry (merge (eq_snd op =))) regs []);
+fun get_mixins thy (name, morph) =
+ let
+ val (regs, mixins) = Registrations.get thy;
+ in
+ case find_first (fn ((name', (morph', export')), _) => ident_eq thy
+ ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
+ NONE => []
+ | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
+ end;
+
+fun collect_mixins thy (name, morph) =
+ roundup thy (fn dep => fn mixins =>
+ merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
+ |> snd |> filter (snd o fst); (* only inheritable mixins *)
+
+fun activate_notes' activ_elem transfer thy export (name, morph) input =
+ let
+ val {notes, ...} = the_locale thy name;
+ fun activate ((kind, facts), _) input =
+ let
+ val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
+ val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
+ in activ_elem (Notes (kind, facts')) input end;
+ in
+ fold_rev activate notes input
+ end;
+
+fun activate_facts' export dep context =
+ let
+ val thy = Context.theory_of context;
+ val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
+ in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
+
+
+(* Diagnostic *)
+
+fun print_registrations thy raw_name =
+ let
+ val name = intern thy raw_name;
+ val name' = extern thy name;
+ val ctxt = ProofContext.init thy;
+ fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
+ fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
+ val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
+ fun prt_term' t = if !show_types
+ then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
+ Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
+ else prt_term t;
+ fun prt_inst ts =
+ Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
+ fun prt_reg (name, morph) =
+ let
+ val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
+ val ts = instance_of thy name morph;
+ in
+ case qs of
+ [] => prt_inst ts
+ | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
+ Pretty.brk 1, prt_inst ts]
+ end;
+ in
+ (case these_registrations thy name of
+ [] => Pretty.str ("no interpretations")
+ | regs => Pretty.big_list "interpretations:" (map prt_reg regs))
+ |> Pretty.writeln
+ end;
(* Add and extend registrations *)
+fun amend_registration (name, morph) mixin export thy =
+ let
+ val regs = Registrations.get thy |> fst;
+ val base = instance_of thy name (morph $> export);
+ fun match ((name', (morph', export')), _) =
+ name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
+ in
+ case find_first match (rev regs) of
+ NONE => error ("No interpretation of locale " ^
+ quote (extern thy name) ^ " and\nparameter instantiation " ^
+ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
+ " available")
+ | SOME (_, stamp') => Registrations.map
+ (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
+ (* FIXME deal with inheritance: propagate to existing children *)
+ end;
+
(* Note that a registration that would be subsumed by an existing one will not be
generated, and it will not be possible to amend it. *)
-fun add_registration (name, base_morph) export thy =
+fun add_registration (name, base_morph) mixin export thy =
let
val base = instance_of thy name base_morph;
in
@@ -378,38 +460,26 @@
then thy
else
let
- val mixins = roundup thy (fn dep => fn mixins =>
- merge (eq_snd op =) (mixins, collect_mixins thy dep)) (name, base_morph) ([], [])
- |> snd |> filter (snd o fst) (* only inheritable mixins *);
- val stamp = stamp ();
+ fun add_reg (dep', morph') =
+ let
+ val mixins = collect_mixins thy (dep', morph' $> export);
+ val stamp = stamp ();
+ in
+ Registrations.map (apfst (cons ((dep', (morph', export)), stamp))
+ #> apsnd (cons (stamp, mixins)))
+ end
in
- thy
- (* add registration and its mixins *)
- |> Registrations.map (apfst (cons ((name, (base_morph, export)), stamp))
- #> apsnd (cons (stamp, mixins)))
+ (get_idents (Context.Theory thy), thy)
+ (* add new registrations with inherited mixins *)
+ |> roundup thy add_reg export (name, base_morph)
+ |> snd
+ (* add mixin *)
+ |> amend_registration (name, base_morph) mixin export
(* activate import hierarchy as far as not already active *)
- |> Context.theory_map (activate_facts (name, base_morph
- $> compose_mixins mixins $> export))
+ |> Context.theory_map (activate_facts' export (name, base_morph))
end
end;
-fun amend_registration mixin (name, base_morph) thy =
- let
- val regs = Registrations.get thy |> fst;
- val base = instance_of thy name base_morph;
- fun match ((name', (morph', _)), _) =
- name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
- in
- case find_first match (rev regs) of
- NONE => error ("No registration of locale " ^
- quote (extern thy name) ^ " and parameter instantiation " ^
- space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
- " available")
- | SOME (_, stamp') => Registrations.map
- (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
- (* FIXME deal with inheritance: propagate to existing children *)
- end;
-
fun amend_registration_legacy morph (name, base_morph) thy =
(* legacy, never modify base morphism *)
let
@@ -435,7 +505,7 @@
in
(get_idents (Context.Theory thy), thy)
|> roundup thy (fn (dep', morph') =>
- Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) (dep, morph)
+ Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph)
|> snd
|> Context.theory_map (activate_facts (dep, morph $> export))
end;
@@ -446,7 +516,7 @@
fun add_dependency loc (dep, morph) export thy =
thy
|> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
- |> (fn thy => fold_rev (Context.theory_map o activate_facts)
+ |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
(all_registrations thy) thy);
(* FIXME deal with inheritance: propagate mixins to new children *)