generic theorem kinds;

--- a/src/Pure/Isar/isar_syn.ML	Sat Oct 13 20:32:07 2001 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 13 20:32:38 2001 +0200
@@ -191,11 +191,11 @@
 
 val theoremsP =
   OuterSyntax.command "theorems" "define theorems" K.thy_decl
-    (name_facts >> (Toplevel.theory o IsarThy.have_theorems));
+    (name_facts >> (Toplevel.theory o IsarThy.have_theorems Drule.theoremK));
 
 val lemmasP =
   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
-    (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
+    (name_facts >> (Toplevel.theory o IsarThy.have_theorems Drule.lemmaK));
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
@@ -288,11 +288,15 @@
 
 val theoremP =
   OuterSyntax.command "theorem" "state theorem" K.thy_goal
-    (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
+    (statement (IsarThy.theorem Drule.theoremK) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val lemmaP =
   OuterSyntax.command "lemma" "state lemma" K.thy_goal
-    (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
+    (statement (IsarThy.theorem Drule.lemmaK) >> (Toplevel.print oo Toplevel.theory_to_proof));
+
+val corollaryP =
+  OuterSyntax.command "corollary" "state corollary" K.thy_goal
+    (statement (IsarThy.theorem Drule.corollaryK) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val showP =
   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
@@ -699,12 +703,13 @@
   typed_print_translationP, print_ast_translationP,
   token_translationP, oracleP,
   (*proof commands*)
-  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
-  defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
-  nextP, qedP, terminal_proofP, default_proofP, immediate_proofP,
-  done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
-  apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
-  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
+  theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, assumeP,
+  presumeP, defP, fixP, letP, caseP, thenP, fromP, withP, noteP,
+  beginP, endP, nextP, qedP, terminal_proofP, default_proofP,
+  immediate_proofP, done_proofP, skip_proofP, forget_proofP, deferP,
+  preferP, applyP, apply_endP, proofP, alsoP, finallyP, moreoverP,
+  ultimatelyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP,
+  undoP, killP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP,

--- a/src/Pure/Isar/isar_thy.ML	Sat Oct 13 20:32:07 2001 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat Oct 13 20:32:38 2001 +0200
@@ -63,15 +63,11 @@
   val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list
   val declare_theorems: (xstring * Args.src list) list * Comment.text -> theory -> theory
   val declare_theorems_i: (thm * theory attribute list) list * Comment.text -> theory -> theory
-  val have_theorems:
+  val have_theorems: string ->
     (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
     -> theory -> theory
-  val have_theorems_i: (((bstring * theory attribute list) * (thm * theory attribute list) list)
-    * Comment.text) list -> theory -> theory
-  val have_lemmas:
-    (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
-    -> theory -> theory
-  val have_lemmas_i: (((bstring * theory attribute list) * (thm * theory attribute list) list)
+  val have_theorems_i:  string ->
+    (((bstring * theory attribute list) * (thm * theory attribute list) list)
     * Comment.text) list -> theory -> theory
   val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list
     -> ProofHistory.T -> ProofHistory.T
@@ -94,13 +90,9 @@
   val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T
   val invoke_case_i: (string * Proof.context attribute list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
-  val theorem: ((bstring * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> bool -> theory -> ProofHistory.T
-  val theorem_i: ((bstring * theory attribute list) * (term * (term list * term list)))
+  val theorem: string -> ((bstring * Args.src list) * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val lemma: ((bstring * Args.src list) * (string * (string list * string list)))
-    * Comment.text -> bool -> theory -> ProofHistory.T
-  val lemma_i: ((bstring * theory attribute list) * (term * (term list * term list)))
+  val theorem_i: string -> ((bstring * theory attribute list) * (term * (term list * term list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
   val assume: (((string * Args.src list) * (string * (string list * string list)) list)
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
@@ -292,14 +284,15 @@
   ((name, map attrib more_srcs), map (fn (s, srcs) => (get s, map attrib srcs)) th_srcs));
 
 fun flat_unnamed (x, ys) = (x, flat (map snd ys));
+fun cond_kind k = if k = "" then [] else [Drule.kind k];
 
 fun global_have_thmss kind f args thy =
   let
     val args' = prep_thmss (PureThy.get_thms thy) (Attrib.global_attribute thy) args
-    val (thy', named_thmss) = f args' thy;
-    fun present (name, thms) = Present.results kind name thms;
+    val (thy', named_thmss) = f (cond_kind kind) args' thy;
+    fun present (name, thms) = Present.results (kind ^ "s") name thms;
   in
-    if kind = "" then ()
+    if kind = "" orelse kind = Drule.internalK then ()
     else Context.setmp (Some thy') (fn () => seq present named_thmss) ();
     (thy', named_thmss)
   end;
@@ -314,22 +307,17 @@
   ((name, more_atts), map (apfst single) th_atts)) args);
 
 fun apply_theorems th_srcs =
-  flat_unnamed o global_have_thmss "" (PureThy.have_thmss []) [(("", []), th_srcs)];
+  flat_unnamed o global_have_thmss "" PureThy.have_thmss [(("", []), th_srcs)];
 fun apply_theorems_i th_srcs =
   flat_unnamed o gen_have_thmss_i (PureThy.have_thmss []) [(("", []), th_srcs)];
 
 val declare_theorems = #1 oo (apply_theorems o Comment.ignore);
 val declare_theorems_i = #1 oo (apply_theorems_i o Comment.ignore);
 
-val have_theorems =
-  #1 oo (global_have_thmss "theorems" (PureThy.have_thmss []) o map Comment.ignore);
-val have_theorems_i =
-  #1 oo (gen_have_thmss_i (PureThy.have_thmss []) o map Comment.ignore);
-
-val have_lemmas =
-  #1 oo (global_have_thmss "lemmas" (PureThy.have_thmss [Drule.tag_lemma]) o map Comment.ignore);
-val have_lemmas_i =
-  #1 oo (gen_have_thmss_i (PureThy.have_thmss [Drule.tag_lemma]) o map Comment.ignore);
+fun have_theorems kind =
+  #1 oo (global_have_thmss kind PureThy.have_thmss o map Comment.ignore);
+fun have_theorems_i kind =
+  #1 oo (gen_have_thmss_i (PureThy.have_thmss (cond_kind kind)) o map Comment.ignore);
 
 val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss o map Comment.ignore;
 val have_facts_i = ProofHistory.apply o gen_have_thmss_i Proof.have_thmss o map Comment.ignore;
@@ -405,13 +393,6 @@
 
 local
 
-fun global_statement f ((name, src), s) int thy =
-  ProofHistory.init (Toplevel.undo_limit int)
-    (f name (map (Attrib.global_attribute thy) src) s thy);
-
-fun global_statement_i f ((name, atts), t) int thy =
-  ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy);
-
 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));
 
@@ -431,10 +412,13 @@
 
 in
 
-val theorem     = global_statement Proof.theorem o Comment.ignore;
-val theorem_i   = global_statement_i Proof.theorem_i o Comment.ignore;
-val lemma       = global_statement Proof.lemma o Comment.ignore;
-val lemma_i     = global_statement_i Proof.lemma_i o Comment.ignore;
+fun theorem k (((name, src), s), comment_ignore) int thy =
+  ProofHistory.init (Toplevel.undo_limit int)
+    (Proof.theorem k name (map (Attrib.global_attribute thy) src) s thy);
+
+fun theorem_i k (((name, atts), t), comment_ignore) int thy =
+  ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k name atts t thy);
+
 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;
@@ -503,7 +487,11 @@
     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;
-  in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
+  in
+    if kind = "" orelse kind = Drule.internalK then ()
+    else (print_result res; Context.setmp (Some thy) (Present.result kind name) thm);
+    thy
+  end);
 
 val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
 val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;

--- a/src/Pure/Isar/proof.ML	Sat Oct 13 20:32:07 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 13 20:32:38 2001 +0200
@@ -81,13 +81,9 @@
   val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val invoke_case: string * context attribute list -> state -> state
-  val theorem: bstring -> theory attribute list -> string * (string list * string list)
-    -> theory -> state
-  val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
+  val theorem: string -> bstring -> theory attribute list -> string * (string list * string list)
     -> theory -> state
-  val lemma: bstring -> theory attribute list -> string * (string list * string list)
-    -> theory -> state
-  val lemma_i: bstring -> theory attribute list -> term * (term list * term list)
+  val theorem_i: string -> bstring -> theory attribute list -> term * (term list * term list)
     -> theory -> state
   val chain: state -> state
   val from_facts: thm list -> state -> state
@@ -127,13 +123,11 @@
 (* type goal *)
 
 datatype kind =
-  Theorem of theory attribute list |    (*top-level theorem*)
-  Lemma of theory attribute list |      (*top-level lemma*)
-  Show of context attribute list |      (*intermediate result, solving subgoal*)
-  Have of context attribute list ;      (*intermediate result*)
+  Theorem of string * theory attribute list |    (*top-level theorem*)
+  Show of context attribute list |               (*intermediate result, solving subgoal*)
+  Have of context attribute list ;               (*intermediate result*)
 
-val kind_name =
-  fn Theorem _ => "theorem" | Lemma _ => "lemma" | Show _ => "show" | Have _ => "have";
+val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have";
 
 type goal =
  (kind *        (*result kind*)
@@ -619,12 +613,10 @@
 
 (*global goals*)
 fun global_goal prepp kind name atts x thy =
-  setup_goal I prepp kind Seq.single name atts x (init_state thy);
+  setup_goal I prepp (curry Theorem kind) Seq.single name atts x (init_state thy);
 
-val theorem = global_goal ProofContext.bind_propp_schematic Theorem;
-val theorem_i = global_goal ProofContext.bind_propp_schematic_i Theorem;
-val lemma = global_goal ProofContext.bind_propp_schematic Lemma;
-val lemma_i = global_goal ProofContext.bind_propp_schematic_i Lemma;
+val theorem = global_goal ProofContext.bind_propp_schematic;
+val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
 
 
 (*local goals*)
@@ -720,9 +712,7 @@
       |> curry Thm.name_thm full_name;
 
     val atts =
-      (case kind of
-        Theorem atts => atts
-      | Lemma atts => atts @ [Drule.tag_lemma]
+      (case kind of Theorem (s, atts) => atts @ [Drule.kind s]
       | _ => err_malformed "finish_global" state);
 
     val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);