# HG changeset patch # User wenzelm # Date 1138384991 -3600 # Node ID 18863b33c831c950d08ec24907a387fbe3850d12 # Parent d42708f5c1869c1a828f992acd71f2e5622c5fdc improved 'notes', including proper treatment of locale results; tuned; diff -r d42708f5c186 -r 18863b33c831 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Jan 27 19:03:10 2006 +0100 +++ b/src/Pure/Isar/local_theory.ML Fri Jan 27 19:03:11 2006 +0100 @@ -7,7 +7,6 @@ signature LOCAL_THEORY = sig - val locale_of: Proof.context -> string option val params_of: Proof.context -> (string * typ) list val hyps_of: Proof.context -> term list val standard: Proof.context -> thm -> thm @@ -16,17 +15,20 @@ val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val init: xstring option -> theory -> Proof.context val init_i: string option -> theory -> Proof.context - val exit: Proof.context -> theory + val exit: Proof.context -> Proof.context * theory val consts: ((string * typ) * mixfix) list -> Proof.context -> term list * Proof.context val axioms: ((string * Attrib.src list) * term list) list -> Proof.context -> (bstring * thm list) list * Proof.context + val axioms_finish: (Proof.context -> thm -> thm) -> + ((string * Attrib.src list) * term list) list -> Proof.context -> + (bstring * thm list) list * Proof.context val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> Proof.context -> (bstring * thm list) list * Proof.context val note: (bstring * Attrib.src list) * thm list -> Proof.context -> (bstring * thm list) * Proof.context val def: (string * mixfix) * ((string * Attrib.src list) * term) -> Proof.context -> (term * (bstring * thm)) * Proof.context - val def': (Proof.context -> term -> thm -> thm) -> + val def_finish: (Proof.context -> term -> thm -> thm) -> (string * mixfix) * ((string * Attrib.src list) * term) -> Proof.context -> (term * (bstring * thm)) * Proof.context end; @@ -34,28 +36,34 @@ structure LocalTheory: LOCAL_THEORY = struct - (** local context data **) structure Data = ProofDataFun ( val name = "Isar/local_theory"; type T = - {locale: string option, + {locale: (string * (cterm list * Proof.context)) option, params: (string * typ) list, hyps: term list, - standard: Proof.context -> thm -> thm, exit: theory -> theory}; - fun init _ = {locale = NONE, params = [], hyps = [], standard = K Drule.standard, exit = I}; + fun init thy = {locale = NONE, params = [], hyps = [], exit = I}; fun print _ _ = (); ); val _ = Context.add_setup Data.init; +fun map_locale f = Data.map (fn {locale, params, hyps, exit} => + {locale = Option.map (fn (loc, (view, ctxt)) => (loc, (view, f ctxt))) locale, + params = params, hyps = hyps, exit = exit}); + val locale_of = #locale o Data.get; val params_of = #params o Data.get; val hyps_of = #hyps o Data.get; -fun standard ctxt = #standard (Data.get ctxt) ctxt; + +fun standard ctxt = + (case #locale (Data.get ctxt) of + NONE => Drule.standard + | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt); (* pretty_consts *) @@ -78,32 +86,44 @@ end; - -(** theory **) +(* theory/locale substructures *) -fun theory f ctxt = - ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt; +fun transfer thy = + ProofContext.transfer thy #> map_locale (ProofContext.transfer thy); + +fun theory f ctxt = transfer (f (ProofContext.theory_of ctxt)) ctxt; fun theory_result f ctxt = let val (res, thy') = f (ProofContext.theory_of ctxt) - in (res, ProofContext.transfer thy' ctxt) end; + in (res, transfer thy' ctxt) end; + +fun locale_result f ctxt = + (case locale_of ctxt of + NONE => error "Local theory: no locale context" + | SOME (loc, (view, loc_ctxt)) => + let + val (res, loc_ctxt') = f loc_ctxt; + val thy' = ProofContext.theory_of loc_ctxt'; + in (res, ctxt |> map_locale (K loc_ctxt') |> transfer thy') end); + + +(* init -- exit *) fun init_i NONE thy = ProofContext.init thy | init_i (SOME loc) thy = thy |> Locale.init loc - |> ProofContext.inferred_fixes - |> (fn (params, ctxt) => Data.put - {locale = SOME loc, + ||>> ProofContext.inferred_fixes + |> (fn ((view, params), ctxt) => Data.put + {locale = SOME (loc, (view, ctxt)), params = params, hyps = ProofContext.assms_of ctxt, - standard = fn inner => ProofContext.export_standard inner ctxt, exit = Sign.restore_naming thy} ctxt) |> theory (Sign.add_path (Sign.base_name loc) #> Sign.no_base_names); -fun init target thy = init_i (Option.map (Locale.intern thy) target) thy; +fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy; -fun exit ctxt = #exit (Data.get ctxt) (ProofContext.theory_of ctxt); +fun exit ctxt = (ctxt, #exit (Data.get ctxt) (ProofContext.theory_of ctxt)); @@ -116,7 +136,7 @@ val thy = ProofContext.theory_of ctxt; val params = params_of ctxt; val ps = map Free params; - val Ps = map snd params; + val Ps = map #2 params; in ctxt |> theory (Sign.add_consts_i (decls |> map (fn ((c, T), mx) => (c, Ps ---> T, mx)))) @@ -125,17 +145,23 @@ end; -(* fact definition *) +(* fact definitions *) fun notes kind facts ctxt = - (case locale_of ctxt of - NONE => ctxt |> theory_result - (PureThy.note_thmss_i (Drule.kind kind) - (Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts)) - | SOME loc => ctxt |> theory_result (Locale.note_thmss_i kind loc facts #> apsnd #1)); + let + val attrib = Attrib.attribute_i (ProofContext.theory_of ctxt); + val facts' = map (apsnd (map (apfst (map (standard ctxt))))) facts; + in + ctxt |> + (case locale_of ctxt of + NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts')) + | SOME (loc, view_ctxt) => + locale_result (K (apfst #1 (Locale.add_thmss kind loc facts' view_ctxt)))) + ||> (#2 o ProofContext.note_thmss_i (Attrib.map_facts attrib facts)) + end; fun note (a, ths) ctxt = - ctxt |> notes Drule.theoremK [(a, [(ths, [])])] |>> hd; + ctxt |> notes PureThy.theoremK [(a, [(ths, [])])] |>> hd; (* axioms *) @@ -162,36 +188,33 @@ in -fun axioms specs ctxt = - let - fun name_list name [x] = [(name, x)] - | name_list name xs = PureThy.name_multi name xs; - val fixes_ctxt = fold (fold ProofContext.fix_frees o snd) specs ctxt; - in - ctxt |> fold_map (fn ((name, atts), props) => - theory_result (fold_map (add_axiom (hyps_of ctxt)) (name_list name props)) - #-> (fn ths => note ((name, atts), map (standard fixes_ctxt) ths))) specs - end; +fun axioms_finish finish = fold_map (fn ((name, atts), props) => + fold ProofContext.fix_frees props + #> (fn ctxt => ctxt + |> theory_result (fold_map (add_axiom (hyps_of ctxt)) (PureThy.name_multi name props)) + |-> (fn ths => note ((name, atts), map (finish ctxt) ths)))); + +val axioms = axioms_finish (K I); end; -(* constant definition *) +(* constant definitions *) local -fun add_def (name, prop) thy = - let - val thy' = thy |> Theory.add_defs_i false [(name, prop)]; - val th = Thm.get_axiom_i thy' (Sign.full_name thy' name); - val cert = Thm.cterm_of thy'; - val subst = map2 (fn var => fn free => (cert (Var var), cert (Free free))) - (Term.add_vars (Thm.prop_of th) []) (Term.add_frees prop []); - in (Drule.cterm_instantiate subst th, thy') end; +fun add_def (name, prop) = + Theory.add_defs_i false [(name, prop)] #> (fn thy => + let + val th = Thm.get_axiom_i thy (Sign.full_name thy name); + val cert = Thm.cterm_of thy; + val subst = map2 (fn var => fn free => (cert (Var var), cert (Free free))) + (Term.add_vars (Thm.prop_of th) []) (Term.add_frees prop []); + in (Drule.cterm_instantiate subst th, thy) end); in -fun def' finish (var, spec) ctxt = +fun def_finish finish (var, spec) ctxt = let val (x, mx) = var; val ((name, atts), rhs) = spec; @@ -205,9 +228,8 @@ #> apfst (fn (b, [th]) => (lhs, (b, th)))) end; +val def = def_finish (K (K I)); + end; -fun def (var, spec) = - def' (fn ctxt => fn _ => standard (ProofContext.fix_frees (snd spec) ctxt)) (var, spec); - end;