# HG changeset patch
# User wenzelm
# Date 1005510785 -3600
# Node ID d8445053eee0d2ead4a0a7cab89257167e22ac44
# Parent  a987beab002d7d0e62bf34e6e6c954ec5f818b48
theorem, have, show etc: multiple statements;

diff -r a987beab002d -r d8445053eee0 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun Nov 11 21:32:12 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Sun Nov 11 21:33:05 2001 +0100
@@ -91,13 +91,22 @@
     -> ProofHistory.T -> ProofHistory.T
   val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
-  val theorem: string -> (xstring * Args.src list) option * Args.src Locale.element list ->
-    ((bstring * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> bool -> theory -> ProofHistory.T
+  val theorem: string -> (xstring * Args.src list) option * Args.src Locale.element list
+    -> ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text
+    -> bool -> theory -> ProofHistory.T
   val theorem_i: string -> (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))) * 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)
+    * 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 ->
-      ((bstring * theory attribute list) * (term * (term list * term list)))
-    * Comment.text -> bool -> theory -> ProofHistory.T
+    (((bstring * Theory.theory Thm.attribute list) *
+      (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
+    -> bool -> theory -> ProofHistory.T
   val assume: (((string * Args.src list) * (string * (string list * string list)) list)
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val assume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list)
@@ -106,26 +115,34 @@
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val presume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list)
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val have: (((string * Args.src list) *
+    (string * (string list * string list)) list) * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
+  val have_i: (((string * Proof.context Thm.attribute list) *
+    (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
+  val hence: (((string * Args.src list) *
+    (string * (string list * string list)) list) * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
+  val hence_i: (((string * Proof.context Thm.attribute list) *
+    (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
+  val show: (((string * Args.src list) *
+    (string * (string list * string list)) list) * Comment.text) list
+    -> bool -> ProofHistory.T -> ProofHistory.T
+  val show_i: (((string * Proof.context Thm.attribute list) *
+    (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
+    -> bool -> ProofHistory.T -> ProofHistory.T
+  val thus: (((string * Args.src list) *
+    (string * (string list * string list)) list) * Comment.text) list
+    -> bool -> ProofHistory.T -> ProofHistory.T
+  val thus_i: (((string * Proof.context Thm.attribute list) *
+    (Term.term * (Term.term list * Term.term list)) list) * Comment.text) list
+    -> bool -> ProofHistory.T -> ProofHistory.T
   val local_def: ((string * Args.src list) * (string * (string * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
   val local_def_i: ((string * Args.src list) * (string * (term * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val show: ((string * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> bool -> ProofHistory.T -> ProofHistory.T
-  val show_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
-    * Comment.text -> bool -> ProofHistory.T -> ProofHistory.T
-  val have: ((string * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val have_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val thus: ((string * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> bool -> ProofHistory.T -> ProofHistory.T
-  val thus_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
-    * Comment.text -> bool -> ProofHistory.T -> ProofHistory.T
-  val hence: ((string * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val hence_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
   val obtain: ((string list * string option) * Comment.text) list
     * (((string * Args.src list) * (string * (string list * string list)) list)
       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
@@ -363,9 +380,13 @@
 
 local
 
-fun pretty_result ctxt {kind, name, thm} =
-  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"),
-    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
+fun pretty_result ctxt k (name, ths) = Pretty.block
+  [Pretty.str (k ^ (if name = "" then "" else " " ^ name ^ ":")), Pretty.brk 1,
+    ProofContext.pretty_thms ctxt ths];
+
+fun pretty_results ctxt (kind, r :: rs) =
+      pretty_result ctxt kind r :: map (pretty_result ctxt "and") rs
+  | pretty_results _ (_, []) = [];
 
 fun pretty_rule s ctxt thm =
   Pretty.block [Pretty.str (s ^ " to solve goal by exported rule:"),
@@ -373,7 +394,7 @@
 
 in
 
-val print_result = Pretty.writeln oo pretty_result;
+val print_result = (Pretty.writeln o Pretty.chunks) oo pretty_results;
 
 fun cond_print_result_rule int =
   if int then (print_result, priority oo (Pretty.string_of oo pretty_rule "Attempt"))
@@ -407,52 +428,56 @@
 
 local
 
-fun local_statement' f g ((name, src), s) int = ProofHistory.apply (fn state =>
-  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s int (g state));
+fun global_attributes thy ((name, src), s) = ((name, map (Attrib.global_attribute thy) src), s);
 
-fun local_statement_i' f g ((name, atts), t) int =
-  ProofHistory.apply (f name atts t int o g);
+fun global_statement f args int thy =
+  ProofHistory.init (Toplevel.undo_limit int) (f (map (global_attributes thy) args) thy);
+fun global_statement_i f args int thy = ProofHistory.init (Toplevel.undo_limit int) (f args thy);
 
-fun local_statement f g args = local_statement' (K ooo f) g args ();
-fun local_statement_i f g args = local_statement_i' (K ooo f) g args ();
-
-fun multi_local_attribute state ((name, src), s) =
+fun local_attributes state ((name, src), s) =
   ((name, map (Attrib.local_attribute (Proof.theory_of state)) src), s);
 
-fun multi_statement f args = ProofHistory.apply (fn state =>
-  f (map (multi_local_attribute state) args) state);
-
-fun multi_statement_i f args = ProofHistory.apply (f args);
+fun local_statement' f g args int = ProofHistory.apply (fn state =>
+  f (map (local_attributes state) args) int (g state));
+fun local_statement_i' f g args int = ProofHistory.apply (f args int o g);
+fun local_statement f g args = local_statement' (K o f) g args ();
+fun local_statement_i f g args = local_statement_i' (K o f) g args ();
 
 in
 
-fun theorem k (locale, elems) (((name, src), s), comment_ignore) int thy =
-  ProofHistory.init (Toplevel.undo_limit int)
-    (Proof.theorem k (apsome (apsnd (map (Attrib.local_attribute thy))) locale)
-      (map (Locale.attribute (Attrib.local_attribute thy)) elems)
-      name (map (Attrib.global_attribute thy) src) s thy);
+fun multi_theorem k (locale, elems) args int thy =
+  global_statement (Proof.multi_theorem k
+    (apsome (apsnd (map (Attrib.local_attribute thy))) locale)
+    (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy;
 
-fun theorem_i k (locale, elems) (((name, atts), t), comment_ignore) int thy =
-  ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k locale elems name atts t thy);
+fun multi_theorem_i k (locale, elems) =
+  global_statement_i (Proof.multi_theorem_i k 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)];
 
-val assume      = multi_statement Proof.assume o map Comment.ignore;
-val assume_i    = multi_statement_i Proof.assume_i o map Comment.ignore;
-val presume     = multi_statement Proof.presume o map Comment.ignore;
-val presume_i   = multi_statement_i Proof.presume_i o map Comment.ignore;
-val local_def   = local_statement Proof.def I o Comment.ignore;
-val local_def_i = local_statement Proof.def_i I o Comment.ignore;
-val show        = local_statement' (Proof.show check_goal Seq.single) I o Comment.ignore;
-val show_i      = local_statement_i' (Proof.show_i check_goal Seq.single) I o Comment.ignore;
-val have        = local_statement (Proof.have Seq.single) I o Comment.ignore;
-val have_i      = local_statement_i (Proof.have_i Seq.single) I o Comment.ignore;
-val thus        = local_statement' (Proof.show check_goal Seq.single) Proof.chain o Comment.ignore;
-val thus_i      = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain o Comment.ignore;
-val hence       = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore;
-val hence_i     = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore;
+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;
+val presume     = local_statement Proof.presume I o map Comment.ignore;
+val presume_i   = local_statement_i Proof.presume_i I o map Comment.ignore;
+val have        = local_statement (Proof.have Seq.single) I o map Comment.ignore;
+val have_i      = local_statement_i (Proof.have_i Seq.single) I o map Comment.ignore;
+val hence       = local_statement (Proof.have Seq.single) Proof.chain o map Comment.ignore;
+val hence_i     = local_statement_i (Proof.have_i Seq.single) Proof.chain o map Comment.ignore;
+val show        = local_statement' (Proof.show check_goal Seq.single) I o map Comment.ignore;
+val show_i      = local_statement_i' (Proof.show_i check_goal Seq.single) I o map Comment.ignore;
+val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain o map Comment.ignore;
+val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain o map Comment.ignore;
+
+fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state =>
+  f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state);
+
+val local_def = gen_def Proof.def o Comment.ignore;
+val local_def_i = gen_def Proof.def_i o Comment.ignore;
 
 fun obtain (xs, asms) = ProofHistory.applys (fn state =>
   Obtain.obtain (map Comment.ignore xs)
-    (map (multi_local_attribute state) (map Comment.ignore asms)) state);
+    (map (local_attributes state) (map Comment.ignore asms)) state);
 
 fun obtain_i (xs, asms) = ProofHistory.applys (fn state =>
   Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms) state);
@@ -509,11 +534,11 @@
   let
     val state = ProofHistory.current prf;
     val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
-    val (thy, res as {kind, name, thm}) = finish state;
+    val (thy, (kind, res)) = finish state;
   in
     if kind = "" orelse kind = Drule.internalK then ()
-    else (print_result (Proof.context_of state) res;
-      Context.setmp (Some thy) (Present.result kind name) thm);
+    else (print_result (Proof.context_of state) (kind, res);
+      Context.setmp (Some thy) Present.multi_result (kind, res));
     thy
   end);