# HG changeset patch
# User wenzelm
# Date 1272055687 -7200
# Node ID 506d732cb52277f1a2298ea18bc6dcfca4d2ecef
# Parent  f9b45eac4c60108dcbd6a17cbf3ab3e71298eae9
explicit 'schematic_theorem' etc. for schematic theorem statements;

diff -r f9b45eac4c60 -r 506d732cb522 NEWS
--- a/NEWS	Fri Apr 23 22:39:49 2010 +0200
+++ b/NEWS	Fri Apr 23 22:48:07 2010 +0200
@@ -6,6 +6,12 @@
 
 *** General ***
 
+* Schematic theorem statements need to be explicitly markup as such,
+via commands 'schematic_lemma', 'schematic_theorem',
+'schematic_corollary'.  Thus the relevance of the proof is made
+syntactically clear, which impacts performance in a parallel or
+asynchronous interactive environment.  Minor INCOMPATIBILITY.
+
 * Authentic syntax for *all* logical entities (type classes, type
 constructors, term constants): provides simple and robust
 correspondence between formal entities and concrete syntax.  Within
diff -r f9b45eac4c60 -r 506d732cb522 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 23 22:39:49 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 23 22:48:07 2010 +0200
@@ -491,16 +491,23 @@
 
 (* statements *)
 
-fun gen_theorem kind =
-  OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
+fun gen_theorem schematic kind =
+  OuterSyntax.local_theory_to_proof'
+    (if schematic then "schematic_" ^ kind else kind)
+    ("state " ^ (if schematic then "schematic " ^ kind else kind))
+    (if schematic then K.thy_schematic_goal else K.thy_goal)
     (Scan.optional (SpecParse.opt_thm_name ":" --|
       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
       SpecParse.general_statement >> (fn (a, (elems, concl)) =>
-        (Specification.theorem_cmd kind NONE (K I) a elems concl)));
+        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
+          kind NONE (K I) a elems concl)));
 
-val _ = gen_theorem Thm.theoremK;
-val _ = gen_theorem Thm.lemmaK;
-val _ = gen_theorem Thm.corollaryK;
+val _ = gen_theorem false Thm.theoremK;
+val _ = gen_theorem false Thm.lemmaK;
+val _ = gen_theorem false Thm.corollaryK;
+val _ = gen_theorem true Thm.theoremK;
+val _ = gen_theorem true Thm.lemmaK;
+val _ = gen_theorem true Thm.corollaryK;
 
 val _ =
   OuterSyntax.command "have" "state local goal"
diff -r f9b45eac4c60 -r 506d732cb522 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Apr 23 22:39:49 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Apr 23 22:48:07 2010 +0200
@@ -62,6 +62,14 @@
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
+  val schematic_theorem: string -> Method.text option ->
+    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
+    Element.context_i list -> Element.statement_i ->
+    bool -> local_theory -> Proof.state
+  val schematic_theorem_cmd: string -> Method.text option ->
+    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
+    Element.context list -> Element.statement ->
+    bool -> local_theory -> Proof.state
   val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
 end;
 
@@ -361,7 +369,7 @@
   fun merge hooks : T = Library.merge (eq_snd op =) hooks;
 );
 
-fun gen_theorem prep_att prep_stmt
+fun gen_theorem schematic prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
   let
     val _ = Local_Theory.affirm lthy;
@@ -397,13 +405,18 @@
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
+    |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
+        error "Illegal schematic goal statement")
     |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
   end;
 
 in
 
-val theorem = gen_theorem (K I) Expression.cert_statement;
-val theorem_cmd = gen_theorem Attrib.intern_src Expression.read_statement;
+val theorem = gen_theorem false (K I) Expression.cert_statement;
+val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
+
+val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
+val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
 
 fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));