--- a/src/Pure/Isar/expression.ML Sun Jan 11 14:18:16 2009 +0100
+++ b/src/Pure/Isar/expression.ML Sun Jan 11 14:18:17 2009 +0100
@@ -12,10 +12,10 @@
type expression = string expr * (Binding.T * string option * mixfix) list;
(* Processing of context statements *)
+ val cert_statement: Element.context_i list -> (term * term list) list list ->
+ Proof.context -> (term * term list) list list * Proof.context;
val read_statement: Element.context list -> (string * string list) list list ->
Proof.context -> (term * term list) list list * Proof.context;
- val cert_statement: Element.context_i list -> (term * term list) list list ->
- Proof.context -> (term * term list) list list * Proof.context;
(* Declaring locales *)
val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
@@ -24,6 +24,9 @@
theory -> string * local_theory;
(* Interpretation *)
+ val cert_goal_expression: expression_i -> Proof.context ->
+ (term list list * (string * morphism) list * morphism) * Proof.context;
+
val sublocale: string -> expression_i -> theory -> Proof.state;
val sublocale_cmd: string -> expression -> theory -> Proof.state;
val interpretation: expression_i -> (Attrib.binding * term) list ->
@@ -740,10 +743,11 @@
map_filter (fn Notes notes => SOME notes | _ => NONE);
val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
+ val axioms = map Element.conclude_witness b_axioms;
val loc_ctxt = thy'
|> Locale.register_locale bname (extraTs, params)
- (asm, rev defs) ([], [])
+ (asm, rev defs) (a_intro, b_intro) axioms ([], [])
(map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
|> TheoryTarget.init (SOME name)
|> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
@@ -816,12 +820,54 @@
val ctxt = ProofContext.init thy;
val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
-
+
val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+ (*** alternative code -- unclear why it does not work yet ***)
+ fun store_reg ((name, morph), thms) thy =
+ let
+ val thms' = map (Element.morph_witness export') thms;
+ val morph' = morph $> Element.satisfy_morphism thms';
+ in
+ thy
+ |> Locale.add_registration (name, (morph', export))
+ |> pair (name, morph')
+ end;
+
+ fun store_eqns_activate regs [] thy =
+ thy
+ |> fold (fn (name, morph) =>
+ Locale.activate_global_facts (name, morph $> export)) regs
+ | store_eqns_activate regs thms thys =
+ let
+ val thms' = thms |> map (Element.conclude_witness #>
+ Morphism.thm (export' $> export) #>
+ LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+ Drule.abs_def);
+ val eq_morph =
+ Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
+ Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+ val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
+ in
+ thy
+ |> fold (fn (name, morph) =>
+ Locale.amend_registration eq_morph (name, morph) #>
+ Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
+ |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn th => [([th], [])]) thms')
+ |> snd
+ end;
+
+ fun after_qed results =
+ let
+ val (wits_reg, wits_eq) = split_last (prep_result (propss @ [eqns]) results);
+ in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg)
+ #-> (fn regs => store_eqns_activate regs wits_eq))
+ end;
+ (*** alternative code end ***)
+
fun store (Reg (name, morph), thms) (regs, thy) =
let
val thms' = map (Element.morph_witness export') thms;
--- a/src/Pure/Isar/locale.ML Sun Jan 11 14:18:16 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Jan 11 14:18:17 2009 +0100
@@ -34,6 +34,7 @@
val register_locale: bstring ->
(string * sort) list * (Binding.T * typ option * mixfix) list ->
term option * term list ->
+ thm option * thm option -> thm list ->
(declaration * stamp) list * (declaration * stamp) list ->
((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
((string * Morphism.morphism) * stamp) list -> theory -> theory
@@ -45,6 +46,8 @@
(* Specification *)
val defined: theory -> string -> bool
val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
+ val intros_of: theory -> string -> thm option * thm option
+ val axioms_of: theory -> string -> thm list
val instance_of: theory -> string -> Morphism.morphism -> term list
val specification_of: theory -> string -> term option * term list
val declarations_of: theory -> string -> declaration list * declaration list
@@ -118,6 +121,8 @@
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
+ intros: thm option * thm option,
+ axioms: thm list,
(** dynamic part **)
decls: (declaration * stamp) list * (declaration * stamp) list,
(* type and term syntax declarations *)
@@ -127,17 +132,18 @@
(* locale dependencies (sublocale relation) *)
};
-fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
- Loc {parameters = parameters, spec = spec, decls = decls,
- notes = notes, dependencies = dependencies};
-fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
- mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
-fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
- Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
- mk_locale ((parameters, spec),
- (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
- merge (eq_snd op =) (notes, notes')),
- merge (eq_snd op =) (dependencies, dependencies')));
+fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
+ Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
+ decls = decls, notes = notes, dependencies = dependencies};
+fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
+ mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
+fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
+ notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
+ dependencies = dependencies', ...}) = mk_locale
+ ((parameters, spec, intros, axioms),
+ (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+ merge (eq_snd op =) (notes, notes')),
+ merge (eq_snd op =) (dependencies, dependencies')));
structure LocalesData = TheoryDataFun
(
@@ -159,9 +165,9 @@
of SOME (Loc loc) => loc
| NONE => error ("Unknown locale " ^ quote name);
-fun register_locale bname parameters spec decls notes dependencies thy =
+fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
- mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
+ mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
fun change_locale name =
LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -175,6 +181,10 @@
fun params_of thy = snd o #parameters o the_locale thy;
+fun intros_of thy = #intros o the_locale thy;
+
+fun axioms_of thy = #axioms o the_locale thy;
+
fun instance_of thy name morph = params_of thy name |>
map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);