--- 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)"
--- 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;
--- 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;
--- 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;
--- 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;
--- 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 ()));