# HG changeset patch # User wenzelm # Date 1463248150 -7200 # Node ID 056ea294c256a7d8b8d702a356736b4c5eb5fe93 # Parent 3081f7719df741f8e1f48a8f5fb5c1a39612c831 toplevel theorem statements support 'if'/'for' eigen-context; diff -r 3081f7719df7 -r 056ea294c256 NEWS --- 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 diff -r 3081f7719df7 -r 056ea294c256 src/Doc/Isar_Ref/Proof.thy --- 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 \ (@@{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} *) \ - 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"}~\a: \\ enters proof mode with \\\ as main goal, eventually resulting in some fact \\ \\ 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>\if\/\<^verbatim>\for\ in postfix + notation, corresponding to \<^verbatim>\assumes\/\<^verbatim>\fixes\ in the long prefix notation. + + Local premises (if present) are called ``\assms\'' for @{syntax + long_statement}, and ``\that\'' for @{syntax short_statement}. \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"} are the same as @{command "lemma"}. The different command names merely serve diff -r 3081f7719df7 -r 056ea294c256 src/HOL/SPARK/Tools/spark_commands.ML --- 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 diff -r 3081f7719df7 -r 056ea294c256 src/Pure/Isar/parse_spec.ML --- 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 *) diff -r 3081f7719df7 -r 056ea294c256 src/Pure/Isar/specification.ML --- 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 diff -r 3081f7719df7 -r 056ea294c256 src/Pure/Pure.thy --- 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 \ 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\ + +ML \ +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) =>