proper predicate definitions of locale body;
authorwenzelm
Tue Jul 16 18:41:00 2002 +0200 (2002-07-16)
changeset 133757cbf2dea46d0
parent 13374 3e270e61133a
child 13376 59975b8417e2
proper predicate definitions of locale body;
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Jul 16 18:40:11 2002 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Jul 16 18:41:00 2002 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  Draws some basic ideas from Florian Kammüller's original version of
     1.5  locales, but uses the richer infrastructure of Isar instead of the raw
     1.6  meta-logic.  Furthermore, we provide structured import of contexts
     1.7 -(with merge and rename operations), as well as type-inference of the
     1.8 -signature parts.
     1.9 +(with merge and rename operations), well as type-inference of the
    1.10 +signature parts, and predicate definitions of the specification text.
    1.11  *)
    1.12  
    1.13  signature LOCALE =
    1.14 @@ -46,8 +46,10 @@
    1.15      string option * context * context * (term * (term list * term list)) list list
    1.16    val print_locales: theory -> unit
    1.17    val print_locale: theory -> expr -> context attribute element list -> unit
    1.18 -  val add_locale: bstring -> expr -> context attribute element list -> theory -> theory
    1.19 -  val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory
    1.20 +  val add_locale: bstring option option -> bstring
    1.21 +    -> expr -> context attribute element list -> theory -> theory
    1.22 +  val add_locale_i: bstring option option -> bstring
    1.23 +    -> expr -> context attribute element_i list -> theory -> theory
    1.24    val smart_have_thmss: string -> (string * 'a) Library.option ->
    1.25      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
    1.26      theory -> theory * (bstring * thm list) list
    1.27 @@ -58,13 +60,14 @@
    1.28      ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
    1.29      theory -> theory * (bstring * thm list) list
    1.30    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
    1.31 -    theory * context -> (theory * context) * thm list list
    1.32 +    theory * context -> (theory * context) * (string * thm list) list
    1.33    val setup: (theory -> theory) list
    1.34  end;
    1.35  
    1.36  structure Locale: LOCALE =
    1.37  struct
    1.38  
    1.39 +
    1.40  (** locale elements and expressions **)
    1.41  
    1.42  type context = ProofContext.context;
    1.43 @@ -201,8 +204,8 @@
    1.44  fun rename_facts prfx elem =
    1.45    let
    1.46      fun qualify (arg as ((name, atts), x)) =
    1.47 -      if name = "" then arg
    1.48 -      else ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x);
    1.49 +      if prfx = "" orelse name = "" orelse NameSpace.is_qualified name then arg
    1.50 +      else ((NameSpace.pack [prfx, name], atts), x);
    1.51    in
    1.52      (case elem of
    1.53        Fixes fixes => Fixes fixes
    1.54 @@ -381,7 +384,7 @@
    1.55            if null ren then ((ps, qs), map #1 elems)
    1.56            else ((map (apfst (rename ren)) ps, map (rename ren) qs),
    1.57              map (rename_elem ren o #1) elems);
    1.58 -        val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems';
    1.59 +        val elems'' = map (rename_facts (space_implode "_" xs)) elems';
    1.60        in ((name, params'), elems'') end;
    1.61  
    1.62      val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
    1.63 @@ -396,25 +399,28 @@
    1.64  
    1.65  local
    1.66  
    1.67 -fun activate_elem (ctxt, Fixes fixes) = (ctxt |> ProofContext.add_fixes fixes, [])
    1.68 -  | activate_elem (ctxt, Assumes asms) =
    1.69 +fun activate_elem _ (ctxt, Fixes fixes) = (ctxt |> ProofContext.add_fixes fixes, [])
    1.70 +  | activate_elem _ (ctxt, Assumes asms) =
    1.71        ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms))
    1.72        |> ProofContext.assume_i ProofContext.export_assume asms
    1.73 -  | activate_elem (ctxt, Defines defs) =
    1.74 +      |> apsnd (map (rpair false))
    1.75 +  | activate_elem _ (ctxt, Defines defs) =
    1.76        ctxt |> ProofContext.assume_i ProofContext.export_def
    1.77 -        (map (fn ((name, atts), (t, ps)) =>
    1.78 +        (defs |> map (fn ((name, atts), (t, ps)) =>
    1.79            let val (c, t') = ProofContext.cert_def ctxt t
    1.80 -          in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs)
    1.81 -  | activate_elem (ctxt, Notes facts) = ctxt |> ProofContext.have_thmss_i facts;
    1.82 +          in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
    1.83 +        |> apsnd (map (rpair false))
    1.84 +  | activate_elem b (ctxt, Notes facts) =
    1.85 +      ctxt |> ProofContext.have_thmss_i facts |> apsnd (map (rpair b));
    1.86  
    1.87  fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt =>
    1.88 -  foldl_map activate_elem (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
    1.89 +  foldl_map (activate_elem (name = "")) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
    1.90      err_in_locale ctxt msg [(name, map fst ps)]);
    1.91  
    1.92  fun activate_elemss prep_facts = foldl_map (fn (ctxt, ((name, ps), raw_elems)) =>
    1.93    let
    1.94      val elems = map (prep_facts ctxt) raw_elems;
    1.95 -    val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), map fst elems) ctxt);
    1.96 +    val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), elems) ctxt);
    1.97    in (ctxt', (((name, ps), elems), facts)) end);
    1.98  
    1.99  in
   1.100 @@ -540,11 +546,8 @@
   1.101  
   1.102  fun eval_text _ _ _ (text, Fixes _) = text
   1.103    | eval_text _ _ do_text ((spec, (xs, env, defs)), Assumes asms) =
   1.104 -      let
   1.105 -        val ts = map (norm_term env) (flat (map (map #1 o #2) asms));
   1.106 -        val spec' = if do_text then spec @ ts else spec;
   1.107 -        val xs' = foldl Term.add_frees (xs, ts);
   1.108 -      in (spec', (xs', env, defs)) end
   1.109 +      let val ts = map (norm_term env) (flat (map (map #1 o #2) asms))
   1.110 +      in (if do_text then spec @ ts else spec, (foldl Term.add_frees (xs, ts), env, defs)) end
   1.111    | eval_text ctxt id _ ((spec, binds), Defines defs) =
   1.112        (spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
   1.113    | eval_text _ _ _ (text, Notes _) = text;
   1.114 @@ -581,25 +584,25 @@
   1.115  fun finish_parms parms ((name, ps), elems) =
   1.116    ((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems);
   1.117  
   1.118 -fun finish_elems ctxt parms _ _ (text, ((id, Int e), _)) =
   1.119 +fun finish_elems ctxt parms _ (text, ((id, Int e), _)) =
   1.120        let
   1.121          val [(_, es)] = unify_elemss ctxt parms [(id, e)];
   1.122          val text' = foldl (eval_text ctxt id false) (text, es);
   1.123        in (text', (id, map Int es)) end
   1.124 -  | finish_elems ctxt parms do_close do_text (text, ((id, Ext e), [propp])) =
   1.125 +  | finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) =
   1.126        let
   1.127          val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
   1.128 -        val text' = eval_text ctxt id do_text (text, e');
   1.129 +        val text' = eval_text ctxt id true (text, e');
   1.130        in (text', (id, [Ext e'])) end;
   1.131  
   1.132  in
   1.133  
   1.134 -fun finish_elemss ctxt parms do_close do_text =
   1.135 -  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close do_text);
   1.136 +fun finish_elemss ctxt parms do_close =
   1.137 +  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
   1.138  
   1.139  end;
   1.140  
   1.141 -fun prep_elemss prep_fixes prepp do_close do_text context fixed_params raw_elemss raw_concl =
   1.142 +fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
   1.143    let
   1.144      val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
   1.145      val raw_propps = map flat raw_proppss;
   1.146 @@ -623,7 +626,7 @@
   1.147      val parms = param_types (xs ~~ typing);
   1.148  
   1.149      val (text, elemss) =
   1.150 -      finish_elemss ctxt parms do_close do_text (([], ([], [], [])), raw_elemss ~~ proppss);
   1.151 +      finish_elemss ctxt parms do_close (([], ([], [], [])), raw_elemss ~~ proppss);
   1.152    in ((parms, elemss, concl), text) end;
   1.153  
   1.154  in
   1.155 @@ -643,12 +646,12 @@
   1.156      raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   1.157    else (name, atts);
   1.158  
   1.159 -fun prep_facts _ _ (Int elem) = (elem, false)
   1.160 -  | prep_facts _ _ (Ext (Fixes fixes)) = (Fixes fixes, true)
   1.161 -  | prep_facts _ ctxt (Ext (Assumes asms)) = (Assumes (map (apfst (prep_name ctxt)) asms), true)
   1.162 -  | prep_facts _ ctxt (Ext (Defines defs)) = (Defines (map (apfst (prep_name ctxt)) defs), true)
   1.163 -  | prep_facts get ctxt (Ext (Notes facts)) = (Notes (facts |> map (fn (a, bs) =>
   1.164 -      (prep_name ctxt a, map (apfst (get ctxt)) bs))), true);
   1.165 +fun prep_facts _ _ (Int elem) = elem
   1.166 +  | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes
   1.167 +  | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms)
   1.168 +  | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs)
   1.169 +  | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) =>
   1.170 +      (prep_name ctxt a, map (apfst (get ctxt)) bs)));
   1.171  
   1.172  in
   1.173  
   1.174 @@ -663,9 +666,10 @@
   1.175  local
   1.176  
   1.177  fun prep_context_statement prep_expr prep_elemss prep_facts
   1.178 -    do_close do_text fixed_params import elements raw_concl context =
   1.179 +    do_close fixed_params import elements raw_concl context =
   1.180    let
   1.181      val sign = ProofContext.sign_of context;
   1.182 +
   1.183      fun flatten (ids, Elem (Fixes fixes)) =
   1.184            (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
   1.185        | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
   1.186 @@ -674,10 +678,12 @@
   1.187  
   1.188      val (import_ids, raw_import_elemss) = flatten ([], Expr import);
   1.189      val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
   1.190 -    val ((parms, all_elemss, concl), (spec, (xs, _, defs))) = prep_elemss do_close do_text
   1.191 +    val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
   1.192        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   1.193 -    val xs' = parms |> mapfilter (fn (p, _) =>
   1.194 -      (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
   1.195 +
   1.196 +    val xs = foldl Term.add_frees ([], spec);
   1.197 +    val xs' = parms |> mapfilter (fn (x, _) =>
   1.198 +      (case assoc_string (xs, x) of None => None | Some T => Some (x, T)));
   1.199  
   1.200      val n = length raw_import_elemss;
   1.201      val (import_ctxt, (import_elemss, import_facts)) =
   1.202 @@ -694,8 +700,8 @@
   1.203  
   1.204  fun gen_facts prep_locale thy name =
   1.205    let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init
   1.206 -    |> gen_context_i false false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
   1.207 -  in flat (map #2 facts) end;
   1.208 +    |> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
   1.209 +  in flat (map (#2 o #1) facts) end;
   1.210  
   1.211  fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
   1.212    let
   1.213 @@ -705,13 +711,13 @@
   1.214        (case locale of None => ([], empty)
   1.215        | Some name => (param_types (#1 (#params (the_locale thy name))), Locale name));
   1.216      val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
   1.217 -      prep_ctxt false false fixed_params import elems concl ctxt;
   1.218 +      prep_ctxt false fixed_params import elems concl ctxt;
   1.219    in (locale, locale_ctxt, elems_ctxt, concl') end;
   1.220  
   1.221  in
   1.222  
   1.223 -fun read_context b x y z = #1 (gen_context true b [] x y [] z);
   1.224 -fun cert_context b x y z = #1 (gen_context_i true b [] x y [] z);
   1.225 +fun read_context x y z = #1 (gen_context true [] x y [] z);
   1.226 +fun cert_context x y z = #1 (gen_context_i true [] x y [] z);
   1.227  val locale_facts = gen_facts intern;
   1.228  val locale_facts_i = gen_facts (K I);
   1.229  val read_context_statement = gen_statement intern gen_context;
   1.230 @@ -729,9 +735,8 @@
   1.231    let
   1.232      val sg = Theory.sign_of thy;
   1.233      val thy_ctxt = ProofContext.init thy;
   1.234 -    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) =
   1.235 -      read_context false import body thy_ctxt;
   1.236 -    val all_elems = map #1 (flat (map #2 (import_elemss @ elemss)));
   1.237 +    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) = read_context import body thy_ctxt;
   1.238 +    val all_elems = flat (map #2 (import_elemss @ elemss));
   1.239  
   1.240      val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
   1.241      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   1.242 @@ -773,9 +778,9 @@
   1.243  
   1.244  in
   1.245  
   1.246 -fun have_thmss_qualified kind loc args thy =
   1.247 +fun have_thmss_qualified kind name args thy =
   1.248    thy
   1.249 -  |> Theory.add_path (Sign.base_name loc)
   1.250 +  |> Theory.add_path (Sign.base_name name)
   1.251    |> PureThy.have_thmss_i (Drule.kind kind) args
   1.252    |>> hide_bound_names (map (#1 o #1) args)
   1.253    |>> Theory.parent_path;
   1.254 @@ -798,9 +803,9 @@
   1.255    let
   1.256      val thy_ctxt = ProofContext.init thy;
   1.257      val loc = prep_locale (Theory.sign_of thy) raw_loc;
   1.258 -    val loc_ctxt = #1 (#1 (#1 (cert_context false (Locale loc) [] thy_ctxt)));
   1.259 +    val loc_ctxt = #1 (#1 (#1 (cert_context (Locale loc) [] thy_ctxt)));
   1.260      val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
   1.261 -    val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt;
   1.262 +    val export = ProofContext.export_standard loc_ctxt thy_ctxt;
   1.263      val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
   1.264      val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
   1.265    in
   1.266 @@ -818,45 +823,116 @@
   1.267    let
   1.268      val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
   1.269      val thy' = put_facts loc args' thy;
   1.270 -    val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [(Notes args', false)])]);
   1.271 -  in ((thy', ctxt'), map #2 facts') end;
   1.272 +    val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [Notes args'])]);
   1.273 +  in ((thy', ctxt'), map #1 facts') end;
   1.274  
   1.275  end;
   1.276  
   1.277  
   1.278  (* predicate text *)
   1.279  
   1.280 -val predN = suffix "_axioms";
   1.281 +local
   1.282 +
   1.283 +val introN = "intro";
   1.284 +val axiomsN = "axioms";
   1.285 +
   1.286 +fun atomize_spec sign ts =
   1.287 +  let
   1.288 +    val t = Library.foldr1 Logic.mk_conjunction ts;
   1.289 +    val body = ObjectLogic.atomize_term sign t;
   1.290 +    val bodyT = Term.fastype_of body;
   1.291 +  in
   1.292 +    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t))
   1.293 +    else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t))
   1.294 +  end;
   1.295 +
   1.296 +fun print_translation name xs thy =
   1.297 +  let
   1.298 +    val n = length xs;
   1.299 +    fun aprop_tr' c = (c, fn args =>
   1.300 +      if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
   1.301 +      else raise Match);
   1.302 +  in thy |> Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' name), []) end;
   1.303  
   1.304 -fun define_pred _ _ _ [] thy = thy
   1.305 -  | define_pred bname name xs ts thy =
   1.306 -      let
   1.307 -        val sign = Theory.sign_of thy;
   1.308 +in
   1.309 +
   1.310 +fun define_pred bname loc (xs, ts, defs) elemss thy =
   1.311 +  let
   1.312 +    val sign = Theory.sign_of thy;
   1.313 +    val name = Sign.full_name sign bname;
   1.314 +
   1.315 +
   1.316 +    (* predicate definition and syntax *)
   1.317  
   1.318 -        val body = ObjectLogic.atomize_term sign (Library.foldr1 Logic.mk_conjunction ts);
   1.319 -        val bodyT = Term.fastype_of body;
   1.320 -        val predT = map #2 xs ---> bodyT;
   1.321 +    val (body, bodyT, body_eq) = atomize_spec sign ts;
   1.322 +    val predT = map #2 xs ---> bodyT;
   1.323 +    val head = Term.list_comb (Const (name, predT), map Free xs);
   1.324 +    val statement = ObjectLogic.assert_propT sign head;
   1.325 +
   1.326 +    val (defs_thy, [pred_def]) =
   1.327 +      thy
   1.328 +      |> (if bodyT = propT then print_translation name xs else I)
   1.329 +      |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
   1.330 +      |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
   1.331 +    val defs_sign = Theory.sign_of defs_thy;
   1.332 +    val cert = Thm.cterm_of defs_sign;
   1.333 +
   1.334  
   1.335 -        val n = length xs;
   1.336 -        fun aprop_tr' c = (c, fn args =>
   1.337 -          if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
   1.338 -          else raise Match);
   1.339 -      in
   1.340 -        thy
   1.341 -        |> (if bodyT <> propT then I
   1.342 -            else Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' (predN name)), []))
   1.343 -        |> Theory.add_consts_i [(predN bname, predT, Syntax.NoSyn)]
   1.344 -        |> PureThy.add_defs_i false [((Thm.def_name (predN bname),
   1.345 -            Logic.mk_equals (Term.list_comb (Const (predN name, predT), map Free xs), body)), [])]
   1.346 -        |> #1
   1.347 -      end;
   1.348 +    (* introduction rule *)
   1.349 +
   1.350 +    val intro = Tactic.prove_standard defs_sign (map #1 xs) ts statement (fn _ =>
   1.351 +      Tactic.rewrite_goals_tac [pred_def] THEN
   1.352 +      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   1.353 +      Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts), 0) 1);
   1.354 +
   1.355 +
   1.356 +    (* derived axioms *)
   1.357 +
   1.358 +    val conjuncts =
   1.359 +      Thm.assume (cert statement)
   1.360 +      |> Tactic.rewrite_rule [pred_def]
   1.361 +      |> Thm.equal_elim (Thm.symmetric body_eq)
   1.362 +      |> Drule.conj_elim_precise (length ts);
   1.363 +
   1.364 +    val assumes = elemss |> map (fn (("", _), es) =>
   1.365 +        flat (es |> map (fn Assumes asms => flat (map (map #1 o #2) asms) | _ => []))
   1.366 +      | _ => []) |> flat;
   1.367 +
   1.368 +    val axioms = (assumes ~~ conjuncts) |> map (fn (t, ax) =>
   1.369 +      Tactic.prove defs_sign [] [] t (fn _ =>
   1.370 +        Tactic.rewrite_goals_tac defs THEN
   1.371 +        Tactic.compose_tac (false, ax, 0) 1));
   1.372 +
   1.373 +    val implies_intr_assumes = Drule.implies_intr_list (map cert assumes);
   1.374 +    fun implies_elim_axioms th = Drule.implies_elim_list (implies_intr_assumes th) axioms;
   1.375 +
   1.376 +    fun change_elem (axms, Assumes asms) =
   1.377 +          apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
   1.378 +            let val n = length spec
   1.379 +            in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end))
   1.380 +      | change_elem (axms, Notes facts) =
   1.381 +          (axms, Notes (facts |> map (apsnd (map (apfst (map implies_elim_axioms))))))
   1.382 +      | change_elem e = e;
   1.383 +
   1.384 +    val elemss' = ((axioms, elemss) |> foldl_map
   1.385 +      (fn (axms, (id as ("", _), es)) => foldl_map change_elem (axms, es) |> apsnd (pair id)
   1.386 +        | x => x) |> #2) @
   1.387 +      [(("", []), [Assumes [((NameSpace.pack [loc, axiomsN], []), [(statement, ([], []))])]])];
   1.388 +  in
   1.389 +    defs_thy
   1.390 +    |> have_thmss_qualified "" bname
   1.391 +      [((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
   1.392 +    |> #1 |> rpair elemss'
   1.393 +  end;
   1.394 +
   1.395 +end;
   1.396  
   1.397  
   1.398  (* add_locale(_i) *)
   1.399  
   1.400  local
   1.401  
   1.402 -fun gen_add_locale prep_ctxt prep_expr bname raw_import raw_body thy =
   1.403 +fun gen_add_locale prep_ctxt prep_expr pname bname raw_import raw_body thy =
   1.404    let
   1.405      val sign = Theory.sign_of thy;
   1.406      val name = Sign.full_name sign bname;
   1.407 @@ -864,21 +940,27 @@
   1.408        error ("Duplicate definition of locale " ^ quote name));
   1.409  
   1.410      val thy_ctxt = ProofContext.init thy;
   1.411 -    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))),
   1.412 -      (pred_xs, pred_ts, defs)) = prep_ctxt true raw_import raw_body thy_ctxt;
   1.413 +    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), text) =
   1.414 +      prep_ctxt raw_import raw_body thy_ctxt;
   1.415 +    val elemss = import_elemss @ body_elemss;
   1.416  
   1.417 -    val import_parms = params_of import_elemss;
   1.418 -    val body_parms = params_of body_elemss;
   1.419 -    val all_parms = import_parms @ body_parms;
   1.420 +    val (pred_thy, elemss') =
   1.421 +      if pname = Some None orelse Library.null (#1 text) then (thy, elemss)
   1.422 +      else if pname = None then thy |> define_pred (bname ^ "_axioms") bname text elemss
   1.423 +      else thy |> define_pred (the (the pname)) bname text elemss;
   1.424 +    val elems' = elemss' |> filter (equal "" o #1 o #1) |> map #2 |> flat;
   1.425  
   1.426 -    val import = prep_expr sign raw_import;
   1.427 -    val elems = map fst (flat (map snd body_elemss));
   1.428 +    val pred_ctxt = ProofContext.init pred_thy;
   1.429 +    val (ctxt, (_, facts)) = activate_facts (K I) (pred_ctxt, elemss')
   1.430 +    val export = ProofContext.export_standard ctxt pred_ctxt;
   1.431    in
   1.432 -    thy
   1.433 -    |> define_pred bname name pred_xs pred_ts
   1.434 +    pred_thy
   1.435 +    |> have_thmss_qualified "" name (facts |> filter #2 |> map (fn ((a, ths), _) =>
   1.436 +      ((a, []), [(map export ths, [])]))) |> #1
   1.437      |> declare_locale name
   1.438 -    |> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems)
   1.439 -        (all_parms, map fst body_parms))
   1.440 +    |> put_locale name (make_locale (prep_expr sign raw_import)
   1.441 +        (map (fn e => (e, stamp ())) elems')
   1.442 +        (params_of elemss', map #1 (params_of body_elemss)))
   1.443    end;
   1.444  
   1.445  in