# HG changeset patch
# User wenzelm
# Date 1332360391 -3600
# Node ID 4ef29b0c568f308961b6560c8b27bd4d045cf3f3
# Parent  8a6124d09ff5bbdf549a3ec7ca7ff19080ed8d6c
optional 'includes' element for long theorem statements;
tuned signatures;

diff -r 8a6124d09ff5 -r 4ef29b0c568f src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -61,7 +61,7 @@
     Specification.theorem Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
-      (Binding.name vc_name, []) ctxt stmt true lthy
+      (Binding.name vc_name, []) [] ctxt stmt true lthy
   end;
 
 fun string_of_status NONE = "(unproved)"
diff -r 8a6124d09ff5 -r 4ef29b0c568f src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/HOL/Tools/recdef.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -266,7 +266,7 @@
         " in recdef definition of " ^ quote name);
   in
     Specification.theorem "" NONE (K I)
-      (Binding.conceal (Binding.name bname), atts) []
+      (Binding.conceal (Binding.name bname), atts) [] []
       (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
diff -r 8a6124d09ff5 -r 4ef29b0c568f src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -13,6 +13,8 @@
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
+  val includes: string list -> Proof.context -> Proof.context
+  val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
   val include_: string list -> Proof.state -> Proof.state
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
   val including: string list -> Proof.state -> Proof.state
@@ -84,30 +86,32 @@
 
 local
 
-fun gen_include prep raw_names ctxt =
+fun gen_includes prep args ctxt =
   let
-    val bundle = maps (the_bundle ctxt o prep ctxt) raw_names;
+    val decls = maps (the_bundle ctxt o prep ctxt) args;
     val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
-    val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
+    val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
   in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
 
-fun gen_includes prep raw_names lthy =
+fun gen_context prep args lthy =
   Named_Target.assert lthy
-  |> gen_include prep raw_names
+  |> gen_includes prep args
   |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
 
 in
 
-fun include_ names =
-  Proof.assert_forward #> Proof.map_context (gen_include (K I) names) #> Proof.put_facts NONE;
-fun include_cmd names =
-  Proof.assert_forward #> Proof.map_context (gen_include check names) #> Proof.put_facts NONE;
+val includes = gen_includes (K I);
+val includes_cmd = gen_includes check;
 
-fun including names = Proof.assert_backward #> Proof.map_context (gen_include (K I) names);
-fun including_cmd names = Proof.assert_backward #> Proof.map_context (gen_include check names);
+fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.put_facts NONE;
+fun include_cmd bs =
+  Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.put_facts NONE;
 
-val context_includes = gen_includes (K I);
-val context_includes_cmd = gen_includes check;
+fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
+fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
+
+val context_includes = gen_context (K I);
+val context_includes_cmd = gen_context check;
 
 end;
 
diff -r 8a6124d09ff5 -r 4ef29b0c568f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -16,7 +16,7 @@
     "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
     "advanced", "and", "assumes", "attach", "begin", "binder",
     "constrains", "defines", "fixes", "for", "identifier", "if",
-    "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
+    "imports", "in", "includes", "infix", "infixl", "infixr", "is", "keywords",
     "notes", "obtains", "open", "output", "overloaded", "pervasive",
     "shows", "structure", "unchecked", "uses", "where", "|"]));
 
@@ -552,10 +552,12 @@
      else (kind, Keyword.thy_goal))
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
     (Scan.optional (Parse_Spec.opt_thm_name ":" --|
-      Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
-      Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
+      Scan.ahead (Parse_Spec.includes >> K "" ||
+        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
+      Scan.optional Parse_Spec.includes [] --
+      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
         ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
-          kind NONE (K I) a elems concl)));
+          kind NONE (K I) a includes elems concl)));
 
 val _ = gen_theorem false Thm.theoremK;
 val _ = gen_theorem false Thm.lemmaK;
diff -r 8a6124d09ff5 -r 4ef29b0c568f src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -19,6 +19,7 @@
   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
+  val includes: (xstring * Position.T) list parser
   val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
@@ -79,6 +80,8 @@
 
 (* locale and context elements *)
 
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
+
 val locale_mixfix =
   Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
   Parse.mixfix;
diff -r 8a6124d09ff5 -r 4ef29b0c568f src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -60,19 +60,19 @@
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context_i list -> Element.statement_i ->
+    string list -> Element.context_i list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val theorem_cmd: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context list -> Element.statement ->
+    (xstring * Position.T) list -> 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 ->
+    string list -> 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 ->
+    (xstring * Position.T) list -> Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
 end;
@@ -378,16 +378,18 @@
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
-fun gen_theorem schematic prep_att prep_stmt
-    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
+fun gen_theorem schematic prep_bundle prep_att prep_stmt
+    kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
   let
     val _ = Local_Theory.assert lthy;
     val thy = Proof_Context.theory_of lthy;
 
     val attrib = prep_att thy;
+
     val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
-    val ((more_atts, prems, stmt, facts), goal_ctxt) =
-      prep_statement attrib prep_stmt elems raw_concl lthy;
+    val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
+      |> Bundle.includes (map (prep_bundle lthy) raw_includes)
+      |> prep_statement attrib prep_stmt elems raw_concl;
     val atts = more_atts @ map attrib raw_atts;
 
     fun after_qed' results goal_ctxt' =
@@ -421,12 +423,13 @@
 
 in
 
-val theorem' = gen_theorem false (K I) Expression.cert_statement;
-fun theorem a b c d e f = theorem' a b c d e f;
-val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
+val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
+val theorem_cmd =
+  gen_theorem false Bundle.check 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;
+val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
+val schematic_theorem_cmd =
+  gen_theorem true Bundle.check Attrib.intern_src Expression.read_statement;
 
 fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));