# HG changeset patch
# User wenzelm
# Date 1006199259 -3600
# Node ID 282a92bc5655acadf3b13513d60eae0d01866992
# Parent  c4a2a0686238fd8c91671ee34e573138978ad1f0
multi_theorem: common statement header (covers *all* results);

diff -r c4a2a0686238 -r 282a92bc5655 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 19 20:46:38 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 19 20:47:39 2001 +0100
@@ -302,20 +302,14 @@
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
 
-val theoremP =
-  OuterSyntax.command "theorem" "state theorem" K.thy_goal
-    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
-      uncurry (IsarThy.multi_theorem Drule.theoremK)));
+fun gen_theorem k =
+  OuterSyntax.command k ("state " ^ k) K.thy_goal
+    (P.opt_thm_name ":" -- in_locale_elems -- statement >> (fn ((x, y), z) =>
+      (Toplevel.print o Toplevel.theory_to_proof (IsarThy.multi_theorem k x y z))));
 
-val lemmaP =
-  OuterSyntax.command "lemma" "state lemma" K.thy_goal
-    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
-      uncurry (IsarThy.multi_theorem Drule.lemmaK)));
-
-val corollaryP =
-  OuterSyntax.command "corollary" "state corollary" K.thy_goal
-    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
-      uncurry (IsarThy.multi_theorem Drule.corollaryK)));
+val theoremP = gen_theorem Drule.theoremK;
+val lemmaP = gen_theorem Drule.lemmaK;
+val corollaryP = gen_theorem Drule.corollaryK;
 
 val showP =
   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
diff -r c4a2a0686238 -r 282a92bc5655 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Nov 19 20:46:38 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 19 20:47:39 2001 +0100
@@ -99,11 +99,13 @@
     -> ((bstring * Theory.theory Thm.attribute list) *
       (Term.term * (Term.term list * Term.term list))) * Comment.text
     -> bool -> theory -> ProofHistory.T
-  val multi_theorem: string -> (xstring * Args.src list) option * Args.src Locale.element list ->
-    (((bstring * Args.src list) * (string * (string list * string list)) list)
+  val multi_theorem: string -> (bstring * Args.src list)
+    -> (xstring * Args.src list) option * Args.src Locale.element list
+    -> (((bstring * Args.src list) * (string * (string list * string list)) list)
     * Comment.text) list -> bool -> theory -> ProofHistory.T
-  val multi_theorem_i: string -> (string * Proof.context attribute list) option
-    * Proof.context attribute Locale.element_i list ->
+  val multi_theorem_i: string -> (bstring * theory attribute list)
+    -> (string * Proof.context attribute list) option
+      * Proof.context attribute Locale.element_i list ->
     (((bstring * Theory.theory Thm.attribute list) *
       (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
     -> bool -> theory -> ProofHistory.T
@@ -445,16 +447,16 @@
 
 in
 
-fun multi_theorem k (locale, elems) args int thy =
-  global_statement (Proof.multi_theorem k
+fun multi_theorem k a (locale, elems) args int thy =
+  global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a)
     (apsome (apsnd (map (Attrib.local_attribute thy))) locale)
     (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy;
 
-fun multi_theorem_i k (locale, elems) =
-  global_statement_i (Proof.multi_theorem_i k locale elems) o map Comment.ignore;
+fun multi_theorem_i k a (locale, elems) =
+  global_statement_i (Proof.multi_theorem_i k a locale elems) o map Comment.ignore;
 
-fun theorem k loc ((a, t), cmt) = multi_theorem k loc [((a, [t]), cmt)];
-fun theorem_i k loc ((a, t), cmt) = multi_theorem_i k loc [((a, [t]), cmt)];
+fun theorem k loc ((a, t), cmt) = multi_theorem k a loc [((("", []), [t]), cmt)];
+fun theorem_i k loc ((a, t), cmt) = multi_theorem_i k a loc [((("", []), [t]), cmt)];
 
 val assume      = local_statement Proof.assume I o map Comment.ignore;
 val assume_i    = local_statement_i Proof.assume_i I o map Comment.ignore;
diff -r c4a2a0686238 -r 282a92bc5655 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 19 20:46:38 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 19 20:47:39 2001 +0100
@@ -76,11 +76,11 @@
   val def: string -> context attribute list -> string *  (string * string list) -> state -> state
   val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
   val invoke_case: string * string option list * context attribute list -> state -> state
-  val multi_theorem: string
+  val multi_theorem: string -> bstring * theory attribute list
     -> (xstring * context attribute list) option -> context attribute Locale.element list
     -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
     -> theory -> state
-  val multi_theorem_i: string
+  val multi_theorem_i: string -> bstring * theory attribute list
     -> (string * context attribute list) option -> context attribute Locale.element_i list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
     -> theory -> state
@@ -133,13 +133,18 @@
 (* type goal *)
 
 datatype kind =
-  Theorem of string * (string * context attribute list) option * theory attribute list list |
-    (*theorem with kind, locale target, attributes*)
-  Show of context attribute list list |  (*intermediate result, solving subgoal*)
-  Have of context attribute list list;   (*intermediate result*)
+  Theorem of string *                           (*theorem kind*)
+    (bstring * theory attribute list) *         (*common result binding*)
+    (string * context attribute list) option *  (*target locale*)
+    theory attribute list list |                (*attributes of individual result binding*)
+  Show of context attribute list list |         (*intermediate result, solving subgoal*)
+  Have of context attribute list list;          (*intermediate result*)
 
-fun kind_name _ (Theorem (s, None, _)) = s
-  | kind_name sg (Theorem (s, Some (name, _), _)) = s ^ " (in " ^ Locale.cond_extern sg name ^ ")"
+fun common_name "" = "" | common_name a = " " ^ a;
+
+fun kind_name _ (Theorem (s, (a, _), None, _)) = s ^ common_name a
+  | kind_name sg (Theorem (s, (a, _), Some (name, _), _)) =
+      s ^ common_name a ^ " (in " ^ Locale.cond_extern sg name ^ ")"
   | kind_name _ (Show _) = "show"
   | kind_name _ (Have _) = "have";
 
@@ -342,7 +347,8 @@
       | subgoals n = ", " ^ string_of_int n ^ " subgoals";
 
     fun prt_names names =
-      (case filter_out (equal "") names of [] => "" | nms => " " ^ space_implode " and " nms);
+      (case filter_out (equal "") names of [] => ""
+      | nms => " " ^ enclose "(" ")" (space_implode " and " nms));
 
     fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
       pretty_facts "using " ctxt
@@ -642,7 +648,7 @@
   end;
 
 (*global goals*)
-fun global_goal prepp prep_locale activate kind raw_locale elems args thy =
+fun global_goal prepp prep_locale activate kind a raw_locale elems args thy =
   let val locale = apsome (apfst (prep_locale (Theory.sign_of thy))) raw_locale in
     thy
     |> init_state
@@ -650,7 +656,7 @@
     |> (case locale of Some (name, _) => map_context (Locale.activate_locale_i name) | None => I)
     |> open_block
     |> map_context (activate elems)
-    |> setup_goal I prepp ProofContext.fix_frees (Theorem (kind, locale, map (snd o fst) args))
+    |> setup_goal I prepp ProofContext.fix_frees (Theorem (kind, a, locale, map (snd o fst) args))
       Seq.single (map (fst o fst) args) (map snd args)
   end;
 
@@ -659,8 +665,10 @@
 val multi_theorem_i =
   global_goal ProofContext.bind_propp_schematic_i (K I) Locale.activate_elements_i;
 
-fun theorem k locale elems name atts p = multi_theorem k locale elems [((name, atts), [p])];
-fun theorem_i k locale elems name atts p = multi_theorem_i k locale elems [((name, atts), [p])];
+fun theorem k locale elems name atts p =
+  multi_theorem k (name, atts) locale elems [(("", []), [p])];
+fun theorem_i k locale elems name atts p =
+  multi_theorem_i k (name, atts) locale elems [(("", []), [p])];
 
 
 (*local goals*)
@@ -773,14 +781,15 @@
     val results = locale_results
       |> map (Drule.strip_shyps_warning o export locale_ctxt theory_ctxt);
 
-    val (k, locale, attss) =
+    val (k, (cname, catts), locale, attss) =
       (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
-    val (thy', res') =
+    val (thy1, res') =
       theory_of state
       |> locale_prefix locale (PureThy.have_thmss [Drule.kind k]
           ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)))
       |>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results);
-  in (thy', (k, res')) end;
+    val thy2 = thy1 |> PureThy.add_thmss [((cname, flat (map #2 res')), catts)] |> #1;
+  in (thy2, (k, res')) end;
 
 (*note: clients should inspect first result only, as backtracking may destroy theory*)
 fun global_qed finalize state =