# HG changeset patch
# User wenzelm
# Date 1026837660 -7200
# Node ID 7cbf2dea46d0c9089eb100e3b7a22c9a1b2eb469
# Parent  3e270e61133aca36322ea466f8f30f0e173e1e8c
proper predicate definitions of locale body;

diff -r 3e270e61133a -r 7cbf2dea46d0 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jul 16 18:40:11 2002 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jul 16 18:41:00 2002 +0200
@@ -9,8 +9,8 @@
 Draws some basic ideas from Florian Kammüller's original version of
 locales, but uses the richer infrastructure of Isar instead of the raw
 meta-logic.  Furthermore, we provide structured import of contexts
-(with merge and rename operations), as well as type-inference of the
-signature parts.
+(with merge and rename operations), well as type-inference of the
+signature parts, and predicate definitions of the specification text.
 *)
 
 signature LOCALE =
@@ -46,8 +46,10 @@
     string option * context * context * (term * (term list * term list)) list list
   val print_locales: theory -> unit
   val print_locale: theory -> expr -> context attribute element list -> unit
-  val add_locale: bstring -> expr -> context attribute element list -> theory -> theory
-  val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory
+  val add_locale: bstring option option -> bstring
+    -> expr -> context attribute element list -> theory -> theory
+  val add_locale_i: bstring option option -> bstring
+    -> expr -> context attribute element_i list -> theory -> theory
   val smart_have_thmss: string -> (string * 'a) Library.option ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
@@ -58,13 +60,14 @@
     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
   val add_thmss: string -> ((string * thm list) * context attribute list) list ->
-    theory * context -> (theory * context) * thm list list
+    theory * context -> (theory * context) * (string * thm list) list
   val setup: (theory -> theory) list
 end;
 
 structure Locale: LOCALE =
 struct
 
+
 (** locale elements and expressions **)
 
 type context = ProofContext.context;
@@ -201,8 +204,8 @@
 fun rename_facts prfx elem =
   let
     fun qualify (arg as ((name, atts), x)) =
-      if name = "" then arg
-      else ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x);
+      if prfx = "" orelse name = "" orelse NameSpace.is_qualified name then arg
+      else ((NameSpace.pack [prfx, name], atts), x);
   in
     (case elem of
       Fixes fixes => Fixes fixes
@@ -381,7 +384,7 @@
           if null ren then ((ps, qs), map #1 elems)
           else ((map (apfst (rename ren)) ps, map (rename ren) qs),
             map (rename_elem ren o #1) elems);
-        val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems';
+        val elems'' = map (rename_facts (space_implode "_" xs)) elems';
       in ((name, params'), elems'') end;
 
     val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
@@ -396,25 +399,28 @@
 
 local
 
-fun activate_elem (ctxt, Fixes fixes) = (ctxt |> ProofContext.add_fixes fixes, [])
-  | activate_elem (ctxt, Assumes asms) =
+fun activate_elem _ (ctxt, Fixes fixes) = (ctxt |> ProofContext.add_fixes fixes, [])
+  | activate_elem _ (ctxt, Assumes asms) =
       ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms))
       |> ProofContext.assume_i ProofContext.export_assume asms
-  | activate_elem (ctxt, Defines defs) =
+      |> apsnd (map (rpair false))
+  | activate_elem _ (ctxt, Defines defs) =
       ctxt |> ProofContext.assume_i ProofContext.export_def
-        (map (fn ((name, atts), (t, ps)) =>
+        (defs |> map (fn ((name, atts), (t, ps)) =>
           let val (c, t') = ProofContext.cert_def ctxt t
-          in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs)
-  | activate_elem (ctxt, Notes facts) = ctxt |> ProofContext.have_thmss_i facts;
+          in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
+        |> apsnd (map (rpair false))
+  | activate_elem b (ctxt, Notes facts) =
+      ctxt |> ProofContext.have_thmss_i facts |> apsnd (map (rpair b));
 
 fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt =>
-  foldl_map activate_elem (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
+  foldl_map (activate_elem (name = "")) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
     err_in_locale ctxt msg [(name, map fst ps)]);
 
 fun activate_elemss prep_facts = foldl_map (fn (ctxt, ((name, ps), raw_elems)) =>
   let
     val elems = map (prep_facts ctxt) raw_elems;
-    val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), map fst elems) ctxt);
+    val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), elems) ctxt);
   in (ctxt', (((name, ps), elems), facts)) end);
 
 in
@@ -540,11 +546,8 @@
 
 fun eval_text _ _ _ (text, Fixes _) = text
   | eval_text _ _ do_text ((spec, (xs, env, defs)), Assumes asms) =
-      let
-        val ts = map (norm_term env) (flat (map (map #1 o #2) asms));
-        val spec' = if do_text then spec @ ts else spec;
-        val xs' = foldl Term.add_frees (xs, ts);
-      in (spec', (xs', env, defs)) end
+      let val ts = map (norm_term env) (flat (map (map #1 o #2) asms))
+      in (if do_text then spec @ ts else spec, (foldl Term.add_frees (xs, ts), env, defs)) end
   | eval_text ctxt id _ ((spec, binds), Defines defs) =
       (spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
   | eval_text _ _ _ (text, Notes _) = text;
@@ -581,25 +584,25 @@
 fun finish_parms parms ((name, ps), elems) =
   ((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems);
 
-fun finish_elems ctxt parms _ _ (text, ((id, Int e), _)) =
+fun finish_elems ctxt parms _ (text, ((id, Int e), _)) =
       let
         val [(_, es)] = unify_elemss ctxt parms [(id, e)];
         val text' = foldl (eval_text ctxt id false) (text, es);
       in (text', (id, map Int es)) end
-  | finish_elems ctxt parms do_close do_text (text, ((id, Ext e), [propp])) =
+  | finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) =
       let
         val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
-        val text' = eval_text ctxt id do_text (text, e');
+        val text' = eval_text ctxt id true (text, e');
       in (text', (id, [Ext e'])) end;
 
 in
 
-fun finish_elemss ctxt parms do_close do_text =
-  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close do_text);
+fun finish_elemss ctxt parms do_close =
+  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
 
 end;
 
-fun prep_elemss prep_fixes prepp do_close do_text context fixed_params raw_elemss raw_concl =
+fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
   let
     val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
     val raw_propps = map flat raw_proppss;
@@ -623,7 +626,7 @@
     val parms = param_types (xs ~~ typing);
 
     val (text, elemss) =
-      finish_elemss ctxt parms do_close do_text (([], ([], [], [])), raw_elemss ~~ proppss);
+      finish_elemss ctxt parms do_close (([], ([], [], [])), raw_elemss ~~ proppss);
   in ((parms, elemss, concl), text) end;
 
 in
@@ -643,12 +646,12 @@
     raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   else (name, atts);
 
-fun prep_facts _ _ (Int elem) = (elem, false)
-  | prep_facts _ _ (Ext (Fixes fixes)) = (Fixes fixes, true)
-  | prep_facts _ ctxt (Ext (Assumes asms)) = (Assumes (map (apfst (prep_name ctxt)) asms), true)
-  | prep_facts _ ctxt (Ext (Defines defs)) = (Defines (map (apfst (prep_name ctxt)) defs), true)
-  | prep_facts get ctxt (Ext (Notes facts)) = (Notes (facts |> map (fn (a, bs) =>
-      (prep_name ctxt a, map (apfst (get ctxt)) bs))), true);
+fun prep_facts _ _ (Int elem) = elem
+  | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes
+  | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms)
+  | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs)
+  | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) =>
+      (prep_name ctxt a, map (apfst (get ctxt)) bs)));
 
 in
 
@@ -663,9 +666,10 @@
 local
 
 fun prep_context_statement prep_expr prep_elemss prep_facts
-    do_close do_text fixed_params import elements raw_concl context =
+    do_close fixed_params import elements raw_concl context =
   let
     val sign = ProofContext.sign_of context;
+
     fun flatten (ids, Elem (Fixes fixes)) =
           (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
       | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
@@ -674,10 +678,12 @@
 
     val (import_ids, raw_import_elemss) = flatten ([], Expr import);
     val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
-    val ((parms, all_elemss, concl), (spec, (xs, _, defs))) = prep_elemss do_close do_text
+    val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
       context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
-    val xs' = parms |> mapfilter (fn (p, _) =>
-      (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
+
+    val xs = foldl Term.add_frees ([], spec);
+    val xs' = parms |> mapfilter (fn (x, _) =>
+      (case assoc_string (xs, x) of None => None | Some T => Some (x, T)));
 
     val n = length raw_import_elemss;
     val (import_ctxt, (import_elemss, import_facts)) =
@@ -694,8 +700,8 @@
 
 fun gen_facts prep_locale thy name =
   let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init
-    |> gen_context_i false false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
-  in flat (map #2 facts) end;
+    |> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
+  in flat (map (#2 o #1) facts) end;
 
 fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
   let
@@ -705,13 +711,13 @@
       (case locale of None => ([], empty)
       | Some name => (param_types (#1 (#params (the_locale thy name))), Locale name));
     val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
-      prep_ctxt false false fixed_params import elems concl ctxt;
+      prep_ctxt false fixed_params import elems concl ctxt;
   in (locale, locale_ctxt, elems_ctxt, concl') end;
 
 in
 
-fun read_context b x y z = #1 (gen_context true b [] x y [] z);
-fun cert_context b x y z = #1 (gen_context_i true b [] x y [] z);
+fun read_context x y z = #1 (gen_context true [] x y [] z);
+fun cert_context x y z = #1 (gen_context_i true [] x y [] z);
 val locale_facts = gen_facts intern;
 val locale_facts_i = gen_facts (K I);
 val read_context_statement = gen_statement intern gen_context;
@@ -729,9 +735,8 @@
   let
     val sg = Theory.sign_of thy;
     val thy_ctxt = ProofContext.init thy;
-    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) =
-      read_context false import body thy_ctxt;
-    val all_elems = map #1 (flat (map #2 (import_elemss @ elemss)));
+    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) = read_context import body thy_ctxt;
+    val all_elems = flat (map #2 (import_elemss @ elemss));
 
     val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
@@ -773,9 +778,9 @@
 
 in
 
-fun have_thmss_qualified kind loc args thy =
+fun have_thmss_qualified kind name args thy =
   thy
-  |> Theory.add_path (Sign.base_name loc)
+  |> Theory.add_path (Sign.base_name name)
   |> PureThy.have_thmss_i (Drule.kind kind) args
   |>> hide_bound_names (map (#1 o #1) args)
   |>> Theory.parent_path;
@@ -798,9 +803,9 @@
   let
     val thy_ctxt = ProofContext.init thy;
     val loc = prep_locale (Theory.sign_of thy) raw_loc;
-    val loc_ctxt = #1 (#1 (#1 (cert_context false (Locale loc) [] thy_ctxt)));
+    val loc_ctxt = #1 (#1 (#1 (cert_context (Locale loc) [] thy_ctxt)));
     val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
-    val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt;
+    val export = ProofContext.export_standard loc_ctxt thy_ctxt;
     val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
     val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
   in
@@ -818,45 +823,116 @@
   let
     val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
     val thy' = put_facts loc args' thy;
-    val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [(Notes args', false)])]);
-  in ((thy', ctxt'), map #2 facts') end;
+    val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [Notes args'])]);
+  in ((thy', ctxt'), map #1 facts') end;
 
 end;
 
 
 (* predicate text *)
 
-val predN = suffix "_axioms";
+local
+
+val introN = "intro";
+val axiomsN = "axioms";
+
+fun atomize_spec sign ts =
+  let
+    val t = Library.foldr1 Logic.mk_conjunction ts;
+    val body = ObjectLogic.atomize_term sign t;
+    val bodyT = Term.fastype_of body;
+  in
+    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t))
+    else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t))
+  end;
+
+fun print_translation name xs thy =
+  let
+    val n = length xs;
+    fun aprop_tr' c = (c, fn args =>
+      if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
+      else raise Match);
+  in thy |> Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' name), []) end;
 
-fun define_pred _ _ _ [] thy = thy
-  | define_pred bname name xs ts thy =
-      let
-        val sign = Theory.sign_of thy;
+in
+
+fun define_pred bname loc (xs, ts, defs) elemss thy =
+  let
+    val sign = Theory.sign_of thy;
+    val name = Sign.full_name sign bname;
+
+
+    (* predicate definition and syntax *)
 
-        val body = ObjectLogic.atomize_term sign (Library.foldr1 Logic.mk_conjunction ts);
-        val bodyT = Term.fastype_of body;
-        val predT = map #2 xs ---> bodyT;
+    val (body, bodyT, body_eq) = atomize_spec sign ts;
+    val predT = map #2 xs ---> bodyT;
+    val head = Term.list_comb (Const (name, predT), map Free xs);
+    val statement = ObjectLogic.assert_propT sign head;
+
+    val (defs_thy, [pred_def]) =
+      thy
+      |> (if bodyT = propT then print_translation name xs else I)
+      |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
+      |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
+    val defs_sign = Theory.sign_of defs_thy;
+    val cert = Thm.cterm_of defs_sign;
+
 
-        val n = length xs;
-        fun aprop_tr' c = (c, fn args =>
-          if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
-          else raise Match);
-      in
-        thy
-        |> (if bodyT <> propT then I
-            else Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' (predN name)), []))
-        |> Theory.add_consts_i [(predN bname, predT, Syntax.NoSyn)]
-        |> PureThy.add_defs_i false [((Thm.def_name (predN bname),
-            Logic.mk_equals (Term.list_comb (Const (predN name, predT), map Free xs), body)), [])]
-        |> #1
-      end;
+    (* introduction rule *)
+
+    val intro = Tactic.prove_standard defs_sign (map #1 xs) ts statement (fn _ =>
+      Tactic.rewrite_goals_tac [pred_def] THEN
+      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+      Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts), 0) 1);
+
+
+    (* derived axioms *)
+
+    val conjuncts =
+      Thm.assume (cert statement)
+      |> Tactic.rewrite_rule [pred_def]
+      |> Thm.equal_elim (Thm.symmetric body_eq)
+      |> Drule.conj_elim_precise (length ts);
+
+    val assumes = elemss |> map (fn (("", _), es) =>
+        flat (es |> map (fn Assumes asms => flat (map (map #1 o #2) asms) | _ => []))
+      | _ => []) |> flat;
+
+    val axioms = (assumes ~~ conjuncts) |> map (fn (t, ax) =>
+      Tactic.prove defs_sign [] [] t (fn _ =>
+        Tactic.rewrite_goals_tac defs THEN
+        Tactic.compose_tac (false, ax, 0) 1));
+
+    val implies_intr_assumes = Drule.implies_intr_list (map cert assumes);
+    fun implies_elim_axioms th = Drule.implies_elim_list (implies_intr_assumes th) axioms;
+
+    fun change_elem (axms, Assumes asms) =
+          apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
+            let val n = length spec
+            in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end))
+      | change_elem (axms, Notes facts) =
+          (axms, Notes (facts |> map (apsnd (map (apfst (map implies_elim_axioms))))))
+      | change_elem e = e;
+
+    val elemss' = ((axioms, elemss) |> foldl_map
+      (fn (axms, (id as ("", _), es)) => foldl_map change_elem (axms, es) |> apsnd (pair id)
+        | x => x) |> #2) @
+      [(("", []), [Assumes [((NameSpace.pack [loc, axiomsN], []), [(statement, ([], []))])]])];
+  in
+    defs_thy
+    |> have_thmss_qualified "" bname
+      [((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
+    |> #1 |> rpair elemss'
+  end;
+
+end;
 
 
 (* add_locale(_i) *)
 
 local
 
-fun gen_add_locale prep_ctxt prep_expr bname raw_import raw_body thy =
+fun gen_add_locale prep_ctxt prep_expr pname bname raw_import raw_body thy =
   let
     val sign = Theory.sign_of thy;
     val name = Sign.full_name sign bname;
@@ -864,21 +940,27 @@
       error ("Duplicate definition of locale " ^ quote name));
 
     val thy_ctxt = ProofContext.init thy;
-    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))),
-      (pred_xs, pred_ts, defs)) = prep_ctxt true raw_import raw_body thy_ctxt;
+    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), text) =
+      prep_ctxt raw_import raw_body thy_ctxt;
+    val elemss = import_elemss @ body_elemss;
 
-    val import_parms = params_of import_elemss;
-    val body_parms = params_of body_elemss;
-    val all_parms = import_parms @ body_parms;
+    val (pred_thy, elemss') =
+      if pname = Some None orelse Library.null (#1 text) then (thy, elemss)
+      else if pname = None then thy |> define_pred (bname ^ "_axioms") bname text elemss
+      else thy |> define_pred (the (the pname)) bname text elemss;
+    val elems' = elemss' |> filter (equal "" o #1 o #1) |> map #2 |> flat;
 
-    val import = prep_expr sign raw_import;
-    val elems = map fst (flat (map snd body_elemss));
+    val pred_ctxt = ProofContext.init pred_thy;
+    val (ctxt, (_, facts)) = activate_facts (K I) (pred_ctxt, elemss')
+    val export = ProofContext.export_standard ctxt pred_ctxt;
   in
-    thy
-    |> define_pred bname name pred_xs pred_ts
+    pred_thy
+    |> have_thmss_qualified "" name (facts |> filter #2 |> map (fn ((a, ths), _) =>
+      ((a, []), [(map export ths, [])]))) |> #1
     |> declare_locale name
-    |> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems)
-        (all_parms, map fst body_parms))
+    |> put_locale name (make_locale (prep_expr sign raw_import)
+        (map (fn e => (e, stamp ())) elems')
+        (params_of elemss', map #1 (params_of body_elemss)))
   end;
 
 in