# HG changeset patch # User haftmann # Date 1231679897 -3600 # Node ID 28d7d7572b812732793ca87bd4cb551ae5d1fb33 # Parent 0f7031a3e692090100c1cb627eeef3c42ba2b450 explicit bookkeeping of intro rules and axiom diff -r 0f7031a3e692 -r 28d7d7572b81 src/Pure/Isar/expression.ML --- 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; diff -r 0f7031a3e692 -r 28d7d7572b81 src/Pure/Isar/locale.ML --- 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);