src/Pure/Isar/locale.ML
changeset 27692 c9d461aad7f3
parent 27686 d1dbe31655be
child 27709 2ba55d217705
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Jul 29 08:15:40 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Jul 29 08:15:44 2008 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4      ((string * Attrib.src list) * term list) list
     1.5    val intros: theory -> string -> thm list * thm list
     1.6    val dests: theory -> string -> thm list
     1.7 +  val elems: theory -> string -> Element.context_i list
     1.8  
     1.9    (* Processing of locale statements *)
    1.10    val read_context_statement: xstring option -> Element.context element list ->
    1.11 @@ -1420,6 +1421,7 @@
    1.12  
    1.13  fun dests thy = #dests o the_locale thy;
    1.14  
    1.15 +fun elems thy = map fst o #elems o the_locale thy;
    1.16  
    1.17  fun parameters_of_expr thy expr =
    1.18    let
    1.19 @@ -1565,7 +1567,7 @@
    1.20    |> Sign.qualified_names
    1.21    |> Sign.add_path (NameSpace.base loc ^ "_locale")
    1.22    |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    1.23 -  |> PureThy.note_thmss_i kind args
    1.24 +  |> PureThy.note_thmss kind args
    1.25    ||> Sign.restore_naming thy;
    1.26  
    1.27  fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    1.28 @@ -1778,7 +1780,7 @@
    1.29        thy
    1.30        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    1.31        |> Sign.declare_const [] (bname, predT, NoSyn) |> snd
    1.32 -      |> PureThy.add_defs_i false
    1.33 +      |> PureThy.add_defs false
    1.34          [((Thm.def_name bname, Logic.mk_equals (head, body)), [PureThy.kind_internal])];
    1.35      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    1.36  
    1.37 @@ -1849,7 +1851,10 @@
    1.38            val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
    1.39            val (_, thy'') =
    1.40              thy'
    1.41 -            |> PureThy.note_thmss_qualified Thm.internalK aname [((introN, []), [([intro], [])])];
    1.42 +            |> Sign.add_path aname
    1.43 +            |> Sign.no_base_names
    1.44 +            |> PureThy.note_thmss Thm.internalK [((introN, []), [([intro], [])])]
    1.45 +            ||> Sign.restore_naming thy';
    1.46          in ((elemss', [statement]), a_elem, [intro], thy'') end;
    1.47      val (predicate, stmt', elemss'', b_intro, thy'''') =
    1.48        if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
    1.49 @@ -1864,9 +1869,12 @@
    1.50                 [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
    1.51            val (_, thy'''') =
    1.52              thy'''
    1.53 -            |> PureThy.note_thmss_qualified Thm.internalK pname
    1.54 +            |> Sign.add_path pname
    1.55 +            |> Sign.no_base_names
    1.56 +            |> PureThy.note_thmss Thm.internalK
    1.57                   [((introN, []), [([intro], [])]),
    1.58 -                  ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])];
    1.59 +                  ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
    1.60 +            ||> Sign.restore_naming thy''';
    1.61          in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
    1.62    in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
    1.63  
    1.64 @@ -1920,16 +1928,17 @@
    1.65        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    1.66  
    1.67      val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
    1.68 -    val (elemss'_, defns) = change_defines_elemss thy elemss [];
    1.69 -    val elemss''_ = elemss'_ @ [(("", []), defns)];
    1.70 -    val (((elemss', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
    1.71 -      define_preds predicate_name' text elemss''_ thy;
    1.72 -    fun mk_regs elemss wits = fold_map (fn (id, elems) => fn wts => let
    1.73 -        val ts = flat (map_filter (fn (Assumes asms) =>
    1.74 -          SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
    1.75 -        val (wts1, wts2) = chop (length ts) wts;
    1.76 -      in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
    1.77 -    val regs = mk_regs elemss' pred_axioms
    1.78 +    val (elemss', defns) = change_defines_elemss thy elemss [];
    1.79 +    val elemss'' = elemss' @ [(("", []), defns)];
    1.80 +    val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
    1.81 +      define_preds predicate_name' text elemss'' thy;
    1.82 +    val regs = pred_axioms
    1.83 +      |> fold_map (fn (id, elems) => fn wts => let
    1.84 +             val ts = flat (map_filter (fn (Assumes asms) =>
    1.85 +               SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
    1.86 +             val (wts1, wts2) = chop (length ts) wts;
    1.87 +           in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
    1.88 +      |> fst
    1.89        |> map_filter (fn (("", _), _) => NONE | e => SOME e);
    1.90      fun axiomify axioms elemss =
    1.91        (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
    1.92 @@ -1937,22 +1946,25 @@
    1.93                       SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
    1.94                     val (axs1, axs2) = chop (length ts) axs;
    1.95                   in (axs2, ((id, Assumed axs1), elems)) end)
    1.96 -        |> snd;
    1.97 +      |> snd;
    1.98      val ((_, facts), ctxt) = activate_facts true (K I)
    1.99 -      (axiomify pred_axioms elemss') (ProofContext.init thy');
   1.100 +      (axiomify pred_axioms elemss''') (ProofContext.init thy');
   1.101      val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
   1.102      val export = Thm.close_derivation o Goal.norm_result o
   1.103        singleton (ProofContext.export view_ctxt thy_ctxt);
   1.104      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
   1.105 -    val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
   1.106 +    val elems' = maps #2 (filter (equal "" o #1 o #1) elemss''');
   1.107      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
   1.108      val axs' = map (Element.assume_witness thy') stmt';
   1.109      val loc_ctxt = thy'
   1.110 -      |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
   1.111 +      |> Sign.add_path bname
   1.112 +      |> Sign.no_base_names
   1.113 +      |> PureThy.note_thmss Thm.assumptionK facts' |> snd
   1.114 +      |> Sign.restore_naming thy'
   1.115        |> register_locale name {axiom = axs',
   1.116          imports = empty,
   1.117          elems = map (fn e => (e, stamp ())) elems'',
   1.118 -        params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
   1.119 +        params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
   1.120          lparams = map #1 (params_of' body_elemss),
   1.121          decls = ([], []),
   1.122          regs = regs,
   1.123 @@ -2103,7 +2115,7 @@
   1.124  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   1.125        ProofContext.init
   1.126        get_global_registration
   1.127 -      PureThy.note_thmss_i
   1.128 +      PureThy.note_thmss
   1.129        global_note_prefix_i
   1.130        Attrib.attribute_i
   1.131        put_global_registration add_global_witness add_global_equation