--- a/NEWS Sat May 14 13:52:01 2016 +0200
+++ b/NEWS Sat May 14 19:49:10 2016 +0200
@@ -63,6 +63,12 @@
eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
'function'.
+* Toplevel theorem statements support eigen-context notation with 'if' /
+'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
+traditional long statement form (in prefix). Local premises are called
+"that" or "assms", respectively. Empty premises are *not* bound in the
+context: INCOMPATIBILITY.
+
* Command 'define' introduces a local (non-polymorphic) definition, with
optional abstraction over local parameters. The syntax resembles
'definition' and 'obtain'. It fits better into the Isar language than
--- a/src/Doc/Isar_Ref/Proof.thy Sat May 14 13:52:01 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sat May 14 19:49:10 2016 +0200
@@ -394,7 +394,8 @@
@{rail \<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
- @@{command proposition} | @@{command schematic_goal}) (stmt | statement)
+ @@{command proposition} | @@{command schematic_goal})
+ (long_statement | short_statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
stmt cond_stmt @{syntax for_fixes}
@@ -406,8 +407,11 @@
;
cond_stmt: ((@'if' | @'when') stmt)?
;
- statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
- conclusion
+ short_statement: stmt (@'if' stmt)? @{syntax for_fixes}
+ ;
+ long_statement: @{syntax thmdecl}? context conclusion
+ ;
+ context: (@{syntax_ref "includes"}?) (@{syntax context_elem} *)
;
conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
;
@@ -419,10 +423,19 @@
\<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,
eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target
- context. An additional @{syntax context} specification may build up an
- initial proof context for the subsequent claim; this includes local
- definitions and syntax as well, see also @{syntax "includes"} in
- \secref{sec:bundle} and @{syntax context_elem} in \secref{sec:locale}.
+ context.
+
+ A @{syntax long_statement} may build up an initial proof context for the
+ subsequent claim, potentially including local definitions and syntax; see
+ also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem}
+ in \secref{sec:locale}.
+
+ A @{syntax short_statement} consists of propositions as conclusion, with an
+ option context of premises and parameters, via \<^verbatim>\<open>if\<close>/\<^verbatim>\<open>for\<close> in postfix
+ notation, corresponding to \<^verbatim>\<open>assumes\<close>/\<^verbatim>\<open>fixes\<close> in the long prefix notation.
+
+ Local premises (if present) are called ``\<open>assms\<close>'' for @{syntax
+ long_statement}, and ``\<open>that\<close>'' for @{syntax short_statement}.
\<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}
are the same as @{command "lemma"}. The different command names merely serve
--- a/src/HOL/SPARK/Tools/spark_commands.ML Sat May 14 13:52:01 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Sat May 14 19:49:10 2016 +0200
@@ -48,7 +48,7 @@
val thy = Proof_Context.theory_of lthy;
val (ctxt, stmt) = get_vc thy vc_name
in
- Specification.theorem Thm.theoremK NONE
+ Specification.theorem true Thm.theoremK NONE
(fn thmss => (Local_Theory.background_theory
(SPARK_VCs.mark_proved vc_name (flat thmss))))
(Binding.name vc_name, []) [] ctxt stmt false lthy
--- a/src/Pure/Isar/parse_spec.ML Sat May 14 13:52:01 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Sat May 14 19:49:10 2016 +0200
@@ -31,8 +31,8 @@
val if_statement: (Attrib.binding * (string * string list) list) list parser
val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser
val obtains: Element.obtains parser
- val general_statement: (Element.context list * Element.statement) parser
- val statement_keyword: string parser
+ val long_statement: (Element.context list * Element.statement) parser
+ val long_statement_keyword: string parser
val overloaded: bool parser
end;
@@ -165,13 +165,13 @@
val obtains = Parse.enum1 "|" obtain_case;
-val general_statement =
- statement >> (fn x => ([], Element.Shows x)) ||
+val long_statement =
Scan.repeat context_element --
(Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains ||
Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
-val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
+val long_statement_keyword =
+ locale_keyword || Parse.$$$ "obtains" || Parse.$$$ "shows";
(* options *)
--- a/src/Pure/Isar/specification.ML Sat May 14 13:52:01 2016 +0200
+++ b/src/Pure/Isar/specification.ML Sat May 14 19:49:10 2016 +0200
@@ -59,19 +59,19 @@
(Attrib.binding * (Facts.ref * Token.src list) list) list ->
(binding * string option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
- val theorem: string -> Method.text option ->
+ val theorem: bool -> string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
string list -> Element.context_i list -> Element.statement_i ->
bool -> local_theory -> Proof.state
- val theorem_cmd: string -> Method.text option ->
+ val theorem_cmd: bool -> string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
(xstring * Position.T) list -> Element.context list -> Element.statement ->
bool -> local_theory -> Proof.state
- val schematic_theorem: string -> Method.text option ->
+ val schematic_theorem: bool -> string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
string list -> Element.context_i list -> Element.statement_i ->
bool -> local_theory -> Proof.state
- val schematic_theorem_cmd: string -> Method.text option ->
+ val schematic_theorem_cmd: bool -> string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
(xstring * Position.T) list -> Element.context list -> Element.statement ->
bool -> local_theory -> Proof.state
@@ -383,7 +383,7 @@
end;
fun gen_theorem schematic bundle_includes prep_att prep_stmt
- kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
+ long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
let
val _ = Local_Theory.assert lthy;
@@ -413,10 +413,12 @@
val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
in lthy'' end;
in after_qed results' lthy'' end;
+
+ val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN;
in
goal_ctxt
- |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
- |> snd
+ |> not (null prems) ?
+ (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
|> Proof.theorem 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
--- a/src/Pure/Pure.thy Sat May 14 13:52:01 2016 +0200
+++ b/src/Pure/Pure.thy Sat May 14 19:49:10 2016 +0200
@@ -397,6 +397,38 @@
ML \<open>
local
+val long_keyword =
+ Parse_Spec.includes >> K "" ||
+ Parse_Spec.long_statement_keyword;
+
+val long_statement =
+ Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Attrib.empty_binding --
+ Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
+ >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
+
+val short_statement =
+ Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
+ >> (fn ((shows, assumes), fixes) =>
+ (false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes],
+ Element.Shows shows));
+
+fun theorem spec schematic descr =
+ Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
+ ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
+ ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
+ long Thm.theoremK NONE (K I) binding includes elems concl)));
+
+val _ = theorem @{command_keyword theorem} false "theorem";
+val _ = theorem @{command_keyword lemma} false "lemma";
+val _ = theorem @{command_keyword corollary} false "corollary";
+val _ = theorem @{command_keyword proposition} false "proposition";
+val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
+
+in end\<close>
+
+ML \<open>
+local
+
val _ =
Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
(Parse_Spec.name_facts -- Parse.for_fixes >>
@@ -639,24 +671,6 @@
Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
>> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
-fun theorem spec schematic descr =
- Outer_Syntax.local_theory_to_proof' spec
- ("state " ^ descr)
- (Scan.optional (Parse_Spec.opt_thm_name ":" --|
- 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)
- Thm.theoremK NONE (K I) a includes elems concl)));
-
-val _ = theorem @{command_keyword theorem} false "theorem";
-val _ = theorem @{command_keyword lemma} false "lemma";
-val _ = theorem @{command_keyword corollary} false "corollary";
-val _ = theorem @{command_keyword proposition} false "proposition";
-val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
-
-
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
(structured_statement >> (fn (a, b, c, d) =>