--- a/src/Pure/Isar/locale.ML Tue Aug 23 09:18:44 2005 +0200
+++ b/src/Pure/Isar/locale.ML Wed Aug 24 12:05:48 2005 +0200
@@ -22,6 +22,9 @@
- beta-eta normalisation of interpretation parameters
- dangling type frees in locales
- test subsumption of interpretations when merging theories
+- var vs. fixes in locale to be interpreted (interpretation in locale)
+ (implicit locale expressions generated by multiple registrations)
+- current finish_global adds unwanted lemmas to theory/locale
*)
signature LOCALE =
@@ -65,9 +68,9 @@
(* Diagnostic functions *)
val print_locales: theory -> unit
val print_locale: theory -> expr -> element list -> unit
- val print_global_registrations: string -> theory -> unit
- val print_local_registrations': string -> context -> unit
- val print_local_registrations: string -> context -> unit
+ val print_global_registrations: bool -> string -> theory -> unit
+ val print_local_registrations': bool -> string -> context -> unit
+ val print_local_registrations: bool -> string -> context -> unit
(* Storing results *)
val add_locale_context: bool -> bstring -> expr -> element list -> theory
@@ -98,18 +101,11 @@
val prep_registration_in_locale:
string -> expr -> theory ->
((string * string list) * term list) list * (thm list -> theory -> theory)
-
- (* Diagnostic *)
- val show_wits: bool ref;
end;
structure Locale: LOCALE =
struct
-(** Diagnostic: whether to show witness theorems of registrations **)
-
-val show_wits = ref false;
-
(** locale elements and expressions **)
type context = ProofContext.context;
@@ -198,7 +194,6 @@
(map (Thm.assume o cert o tinst_tab_term tinst) hyps))
end;
-
(* instantiate TFrees and Frees *)
fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst
@@ -249,6 +244,13 @@
end;
+fun inst_tab_att thy (inst as (_, tinst)) =
+ Args.map_values I (tinst_tab_type tinst)
+ (inst_tab_term inst) (inst_tab_thm thy inst);
+
+fun inst_tab_atts thy inst = map (inst_tab_att thy inst);
+
+
(** management of registrations in theories and proof contexts **)
structure Registrations :
@@ -523,7 +525,7 @@
(* printing of registrations *)
-fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt =
+fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
let
val ctxt = mk_ctxt thy_ctxt;
val thy = ProofContext.theory_of ctxt;
@@ -537,11 +539,11 @@
fun prt_thms thms =
Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms));
fun prt_reg (ts, (("", []), thms)) =
- if ! show_wits
+ if show_wits
then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms]
else prt_inst ts
| prt_reg (ts, (attn, thms)) =
- if ! show_wits
+ if show_wits
then Pretty.block ((prt_attn attn @
[Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
prt_thms thms]))
@@ -569,9 +571,9 @@
val print_local_registrations' =
gen_print_registrations LocalLocalesData.get
I "context";
-fun print_local_registrations loc ctxt =
- (print_global_registrations loc (ProofContext.theory_of ctxt);
- print_local_registrations' loc ctxt);
+fun print_local_registrations show_wits loc ctxt =
+ (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
+ print_local_registrations' show_wits loc ctxt);
(* diagnostics *)
@@ -784,9 +786,6 @@
datatype 'a mode = Assumed of 'a | Derived of 'a;
-fun map_mode2 f _ (Assumed x) = Assumed (f x)
- | map_mode2 _ g (Derived x) = Derived (g x);
-
fun map_mode f (Assumed x) = Assumed (f x)
| map_mode f (Derived x) = Derived (f x);
@@ -963,7 +962,6 @@
where name is a locale name, ps a list of parameter names and axs
a list of axioms relating to the identifier, axs is empty unless
identify at top level (top = true);
- ty is the parameter typing (empty if at top level);
parms is accumulated list of parameters *)
let
val {predicate = (_, axioms), import, params, ...} =
@@ -1731,14 +1729,32 @@
end;
+(* collect witness theorems for global registration;
+ requires parameters and flattened list of (assumed!) identifiers
+ instead of recomputing it from the target *)
+
+fun collect_global_witnesses thy parms ids vts = let
+ val ts = map Logic.unvarify vts;
+ val (parms, parmTs) = split_list parms;
+ val parmvTs = map Type.varifyT parmTs;
+ val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
+ val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
+ |> Symtab.make;
+ (* replace parameter names in ids by instantiations *)
+ val vinst = Symtab.make (parms ~~ vts);
+ fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
+ val inst = Symtab.make (parms ~~ ts);
+ val ids' = map (apsnd vinst_names) ids;
+ val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
+ in ((inst, tinst), wits) end;
+
+
(* store instantiations of args for all registered interpretations
of the theory *)
fun note_thmss_registrations kind target args thy =
let
- val (parms, parmTs) =
- the_locale thy target |> #params |> fst |> map fst |> split_list;
- val parmvTs = map Type.varifyT parmTs;
+ val parms = the_locale thy target |> #params |> fst |> map fst;
val ids = flatten (ProofContext.init thy, intern_expr thy)
(([], Symtab.empty), Expr (Locale target)) |> fst |> fst
|> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
@@ -1749,21 +1765,13 @@
fun activate (thy, (vts, ((prfx, atts2), _))) =
let
- val ts = map Logic.unvarify vts;
- (* type instantiation *)
- val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
- val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
- |> Symtab.make;
- (* replace parameter names in ids by instantiations *)
- val vinst = Symtab.make (parms ~~ vts);
- fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
- val inst = Symtab.make (parms ~~ ts);
- val ids' = map (apsnd vinst_names) ids;
- val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
+ val ((inst, tinst), prems) = collect_global_witnesses thy parms ids vts;
val args' = map (fn ((n, atts), [(ths, [])]) =>
((NameSpace.qualified prfx n,
- map (Attrib.global_attribute_i thy) (atts @ atts2)),
- [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm thy (inst, tinst)) ths, [])]))
+ map (Attrib.global_attribute_i thy)
+ (inst_tab_atts thy (inst, tinst) atts @ atts2)),
+ [(map (Drule.standard o Drule.satisfy_hyps prems o
+ inst_tab_thm thy (inst, tinst)) ths, [])]))
args;
in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
in Library.foldl activate (thy, regs) end;
@@ -2027,24 +2035,23 @@
(* extract proof obligations (assms and defs) from elements *)
-fun extract_asms_elem (ts, Fixes _) = ts
- | extract_asms_elem (ts, Constrains _) = ts
- | extract_asms_elem (ts, Assumes asms) =
+fun extract_asms_elem (Fixes _) ts = ts
+ | extract_asms_elem (Constrains _) ts = ts
+ | extract_asms_elem (Assumes asms) ts =
ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
- | extract_asms_elem (ts, Defines defs) =
+ | extract_asms_elem (Defines defs) ts =
ts @ map (fn (_, (def, _)) => def) defs
- | extract_asms_elem (ts, Notes _) = ts;
+ | extract_asms_elem (Notes _) ts = ts;
fun extract_asms_elems ((id, Assumed _), elems) =
- SOME (id, Library.foldl extract_asms_elem ([], elems))
- | extract_asms_elems ((_, Derived _), _) = NONE;
+ (id, fold extract_asms_elem elems [])
+ | extract_asms_elems ((id, Derived _), _) = (id, []);
-fun extract_asms_elemss elemss =
- List.mapPartial extract_asms_elems elemss;
+fun extract_asms_elemss elemss = map extract_asms_elems elemss;
(* activate instantiated facts in theory or context *)
-fun gen_activate_facts_elemss get_reg note_thmss attrib std put_reg add_wit
+fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
attn all_elemss new_elemss propss result thy_ctxt =
let
fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
@@ -2058,10 +2065,10 @@
|> map (apsnd (map (apfst (map disch))))
(* prefix names *)
|> map (apfst (apfst (NameSpace.qualified prfx)))
- in fst (note_thmss prfx facts' thy_ctxt) end
+ in fst (note prfx facts' thy_ctxt) end
| activate_elem _ _ _ thy_ctxt = thy_ctxt;
- fun activate_elems disch ((id, mode), elems) thy_ctxt =
+ fun activate_elems disch ((id, _), elems) thy_ctxt =
let
val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
handle Option => sys_error ("Unknown registration of " ^
@@ -2219,14 +2226,13 @@
(* target already in internal form *)
let
val ctxt = ProofContext.init thy;
- val ((target_ids, target_syn), target_elemss) = flatten (ctxt, I)
+ val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
(([], Symtab.empty), Expr (Locale target));
val fixed = the_locale thy target |> #params |> #1 |> map #1;
val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
- ((target_ids, target_syn), Expr expr);
- val ids = Library.drop (length target_ids, all_ids);
- val ((parms, elemss, _), _) =
- read_elemss false ctxt fixed raw_elemss [];
+ ((raw_target_ids, target_syn), Expr expr);
+ val (target_ids, ids) = splitAt (length raw_target_ids, all_ids);
+ val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
(** compute proof obligations **)
@@ -2236,16 +2242,85 @@
val elemss' = map (fn (_, es) =>
map (fn Int e => e) es) elemss
(* extract assumptions and defs *)
- val propss = extract_asms_elemss (ids' ~~ elemss');
+ val ids_elemss = ids' ~~ elemss';
+ val propss = extract_asms_elemss ids_elemss;
- (** activation function: add registrations **)
+ (** activation function:
+ - add registrations to the target locale
+ - add induced registrations for all global registrations of
+ the target, unless already present
+ - add facts of induced registrations to theory **)
+
+ val t_ids = List.mapPartial
+ (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
+
fun activate locale_results thy = let
- val thmss = unflat (map snd propss) locale_results;
- fun activate_id (id, thms) thy =
+ val ids_elemss_thmss = ids_elemss ~~
+ unflat (map snd propss) locale_results;
+ val regs = get_global_registrations thy target;
+
+ fun activate_id (((id, Assumed _), _), thms) thy =
thy |> put_registration_in_locale target id
- |> fold (add_witness_in_locale target id) thms;
+ |> fold (add_witness_in_locale target id) thms
+ | activate_id _ thy = thy;
+
+ fun activate_reg (vts, ((prfx, atts2), _)) thy = let
+ val ((inst, tinst), wits) =
+ collect_global_witnesses thy fixed t_ids vts;
+ fun inst_parms ps = map (fn p =>
+ valOf (assoc (map #1 fixed ~~ vts, p))) ps;
+ val disch = Drule.fconv_rule (Thm.beta_conversion true) o
+ Drule.satisfy_hyps wits;
+ val new_elemss = List.filter (fn (((name, ps), _), _) =>
+ not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
+ fun activate_assumed_id (((_, Derived _), _), _) thy = thy
+ | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
+ val ps' = inst_parms ps;
+ in
+ if test_global_registration thy (name, ps')
+ then thy
+ else thy
+ |> put_global_registration (name, ps') (prfx, atts2)
+ |> fold (fn thm => fn thy => add_global_witness (name, ps')
+ ((disch o inst_tab_thm thy (inst, tinst)) thm) thy) thms
+ end;
+
+ fun activate_derived_id ((_, Assumed _), _) thy = thy
+ | activate_derived_id (((name, ps), Derived ths), _) thy = let
+ val ps' = inst_parms ps;
+ in
+ if test_global_registration thy (name, ps')
+ then thy
+ else thy
+ |> put_global_registration (name, ps') (prfx, atts2)
+ |> fold (fn thm => fn thy => add_global_witness (name, ps')
+ ((disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results) thm) thy) ths
+ end;
+
+ fun activate_elem (Notes facts) thy =
+ let
+ val facts' = facts
+ |> Attrib.map_facts (Attrib.global_attribute_i thy o
+ Args.map_values I (tinst_tab_type tinst)
+ (inst_tab_term (inst, tinst))
+ (disch o inst_tab_thm thy (inst, tinst) o
+ Drule.satisfy_hyps locale_results))
+ |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2)))
+ |> map (apsnd (map (apfst (map (disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results)))))
+ |> map (apfst (apfst (NameSpace.qualified prfx)))
+ in
+ fst (global_note_accesses_i (Drule.kind "") prfx facts' thy)
+ end
+ | activate_elem _ thy = thy;
+
+ fun activate_elems (_, elems) thy = fold activate_elem elems thy;
+
+ in thy |> fold activate_assumed_id ids_elemss_thmss
+ |> fold activate_derived_id ids_elemss
+ |> fold activate_elems new_elemss end;
in
- fold activate_id (map fst propss ~~ thmss) thy
+ thy |> fold activate_id ids_elemss_thmss
+ |> fold activate_reg regs
end;
in (propss, activate) end;