toplevel theorem statements support 'if'/'for' eigen-context;
authorwenzelm
Sat May 14 19:49:10 2016 +0200 (2016-05-14 ago)
changeset 63094056ea294c256
parent 63093 3081f7719df7
child 63095 201480e65b7d
toplevel theorem statements support 'if'/'for' eigen-context;
NEWS
src/Doc/Isar_Ref/Proof.thy
src/HOL/SPARK/Tools/spark_commands.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/specification.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sat May 14 13:52:01 2016 +0200
     1.2 +++ b/NEWS	Sat May 14 19:49:10 2016 +0200
     1.3 @@ -63,6 +63,12 @@
     1.4  eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
     1.5  'function'.
     1.6  
     1.7 +* Toplevel theorem statements support eigen-context notation with 'if' /
     1.8 +'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
     1.9 +traditional long statement form (in prefix). Local premises are called
    1.10 +"that" or "assms", respectively. Empty premises are *not* bound in the
    1.11 +context: INCOMPATIBILITY.
    1.12 +
    1.13  * Command 'define' introduces a local (non-polymorphic) definition, with
    1.14  optional abstraction over local parameters. The syntax resembles
    1.15  'definition' and 'obtain'. It fits better into the Isar language than
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat May 14 13:52:01 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat May 14 19:49:10 2016 +0200
     2.3 @@ -394,7 +394,8 @@
     2.4  
     2.5    @{rail \<open>
     2.6      (@@{command lemma} | @@{command theorem} | @@{command corollary} |
     2.7 -     @@{command proposition} | @@{command schematic_goal}) (stmt | statement)
     2.8 +     @@{command proposition} | @@{command schematic_goal})
     2.9 +      (long_statement | short_statement)
    2.10      ;
    2.11      (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
    2.12        stmt cond_stmt @{syntax for_fixes}
    2.13 @@ -406,8 +407,11 @@
    2.14      ;
    2.15      cond_stmt: ((@'if' | @'when') stmt)?
    2.16      ;
    2.17 -    statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
    2.18 -      conclusion
    2.19 +    short_statement: stmt (@'if' stmt)? @{syntax for_fixes}
    2.20 +    ;
    2.21 +    long_statement: @{syntax thmdecl}? context conclusion
    2.22 +    ;
    2.23 +    context: (@{syntax_ref "includes"}?) (@{syntax context_elem} *)
    2.24      ;
    2.25      conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
    2.26      ;
    2.27 @@ -419,10 +423,19 @@
    2.28  
    2.29    \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,
    2.30    eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target
    2.31 -  context. An additional @{syntax context} specification may build up an
    2.32 -  initial proof context for the subsequent claim; this includes local
    2.33 -  definitions and syntax as well, see also @{syntax "includes"} in
    2.34 -  \secref{sec:bundle} and @{syntax context_elem} in \secref{sec:locale}.
    2.35 +  context.
    2.36 +
    2.37 +  A @{syntax long_statement} may build up an initial proof context for the
    2.38 +  subsequent claim, potentially including local definitions and syntax; see
    2.39 +  also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem}
    2.40 +  in \secref{sec:locale}.
    2.41 +
    2.42 +  A @{syntax short_statement} consists of propositions as conclusion, with an
    2.43 +  option context of premises and parameters, via \<^verbatim>\<open>if\<close>/\<^verbatim>\<open>for\<close> in postfix
    2.44 +  notation, corresponding to \<^verbatim>\<open>assumes\<close>/\<^verbatim>\<open>fixes\<close> in the long prefix notation.
    2.45 +
    2.46 +  Local premises (if present) are called ``\<open>assms\<close>'' for @{syntax
    2.47 +  long_statement}, and ``\<open>that\<close>'' for @{syntax short_statement}.
    2.48  
    2.49    \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}
    2.50    are the same as @{command "lemma"}. The different command names merely serve
     3.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Sat May 14 13:52:01 2016 +0200
     3.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat May 14 19:49:10 2016 +0200
     3.3 @@ -48,7 +48,7 @@
     3.4      val thy = Proof_Context.theory_of lthy;
     3.5      val (ctxt, stmt) = get_vc thy vc_name
     3.6    in
     3.7 -    Specification.theorem Thm.theoremK NONE
     3.8 +    Specification.theorem true Thm.theoremK NONE
     3.9        (fn thmss => (Local_Theory.background_theory
    3.10           (SPARK_VCs.mark_proved vc_name (flat thmss))))
    3.11        (Binding.name vc_name, []) [] ctxt stmt false lthy
     4.1 --- a/src/Pure/Isar/parse_spec.ML	Sat May 14 13:52:01 2016 +0200
     4.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat May 14 19:49:10 2016 +0200
     4.3 @@ -31,8 +31,8 @@
     4.4    val if_statement: (Attrib.binding * (string * string list) list) list parser
     4.5    val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser
     4.6    val obtains: Element.obtains parser
     4.7 -  val general_statement: (Element.context list * Element.statement) parser
     4.8 -  val statement_keyword: string parser
     4.9 +  val long_statement: (Element.context list * Element.statement) parser
    4.10 +  val long_statement_keyword: string parser
    4.11    val overloaded: bool parser
    4.12  end;
    4.13  
    4.14 @@ -165,13 +165,13 @@
    4.15  
    4.16  val obtains = Parse.enum1 "|" obtain_case;
    4.17  
    4.18 -val general_statement =
    4.19 -  statement >> (fn x => ([], Element.Shows x)) ||
    4.20 +val long_statement =
    4.21    Scan.repeat context_element --
    4.22     (Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains ||
    4.23      Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
    4.24  
    4.25 -val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
    4.26 +val long_statement_keyword =
    4.27 +  locale_keyword || Parse.$$$ "obtains" || Parse.$$$ "shows";
    4.28  
    4.29  
    4.30  (* options *)
     5.1 --- a/src/Pure/Isar/specification.ML	Sat May 14 13:52:01 2016 +0200
     5.2 +++ b/src/Pure/Isar/specification.ML	Sat May 14 19:49:10 2016 +0200
     5.3 @@ -59,19 +59,19 @@
     5.4      (Attrib.binding * (Facts.ref * Token.src list) list) list ->
     5.5      (binding * string option * mixfix) list ->
     5.6      bool -> local_theory -> (string * thm list) list * local_theory
     5.7 -  val theorem: string -> Method.text option ->
     5.8 +  val theorem: bool -> string -> Method.text option ->
     5.9      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    5.10      string list -> Element.context_i list -> Element.statement_i ->
    5.11      bool -> local_theory -> Proof.state
    5.12 -  val theorem_cmd: string -> Method.text option ->
    5.13 +  val theorem_cmd: bool -> string -> Method.text option ->
    5.14      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    5.15      (xstring * Position.T) list -> Element.context list -> Element.statement ->
    5.16      bool -> local_theory -> Proof.state
    5.17 -  val schematic_theorem: string -> Method.text option ->
    5.18 +  val schematic_theorem: bool -> string -> Method.text option ->
    5.19      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    5.20      string list -> Element.context_i list -> Element.statement_i ->
    5.21      bool -> local_theory -> Proof.state
    5.22 -  val schematic_theorem_cmd: string -> Method.text option ->
    5.23 +  val schematic_theorem_cmd: bool -> string -> Method.text option ->
    5.24      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    5.25      (xstring * Position.T) list -> Element.context list -> Element.statement ->
    5.26      bool -> local_theory -> Proof.state
    5.27 @@ -383,7 +383,7 @@
    5.28    end;
    5.29  
    5.30  fun gen_theorem schematic bundle_includes prep_att prep_stmt
    5.31 -    kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
    5.32 +    long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
    5.33    let
    5.34      val _ = Local_Theory.assert lthy;
    5.35  
    5.36 @@ -413,10 +413,12 @@
    5.37                val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
    5.38              in lthy'' end;
    5.39        in after_qed results' lthy'' end;
    5.40 +
    5.41 +    val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN;
    5.42    in
    5.43      goal_ctxt
    5.44 -    |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
    5.45 -    |> snd
    5.46 +    |> not (null prems) ?
    5.47 +      (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
    5.48      |> Proof.theorem before_qed after_qed' (map snd stmt)
    5.49      |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
    5.50      |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
     6.1 --- a/src/Pure/Pure.thy	Sat May 14 13:52:01 2016 +0200
     6.2 +++ b/src/Pure/Pure.thy	Sat May 14 19:49:10 2016 +0200
     6.3 @@ -397,6 +397,38 @@
     6.4  ML \<open>
     6.5  local
     6.6  
     6.7 +val long_keyword =
     6.8 +  Parse_Spec.includes >> K "" ||
     6.9 +  Parse_Spec.long_statement_keyword;
    6.10 +
    6.11 +val long_statement =
    6.12 +  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Attrib.empty_binding --
    6.13 +  Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
    6.14 +    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
    6.15 +
    6.16 +val short_statement =
    6.17 +  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
    6.18 +    >> (fn ((shows, assumes), fixes) =>
    6.19 +      (false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes],
    6.20 +        Element.Shows shows));
    6.21 +
    6.22 +fun theorem spec schematic descr =
    6.23 +  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
    6.24 +    ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
    6.25 +      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    6.26 +        long Thm.theoremK NONE (K I) binding includes elems concl)));
    6.27 +
    6.28 +val _ = theorem @{command_keyword theorem} false "theorem";
    6.29 +val _ = theorem @{command_keyword lemma} false "lemma";
    6.30 +val _ = theorem @{command_keyword corollary} false "corollary";
    6.31 +val _ = theorem @{command_keyword proposition} false "proposition";
    6.32 +val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
    6.33 +
    6.34 +in end\<close>
    6.35 +
    6.36 +ML \<open>
    6.37 +local
    6.38 +
    6.39  val _ =
    6.40    Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
    6.41      (Parse_Spec.name_facts -- Parse.for_fixes >>
    6.42 @@ -639,24 +671,6 @@
    6.43    Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
    6.44      >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
    6.45  
    6.46 -fun theorem spec schematic descr =
    6.47 -  Outer_Syntax.local_theory_to_proof' spec
    6.48 -    ("state " ^ descr)
    6.49 -    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
    6.50 -      Scan.ahead (Parse_Spec.includes >> K "" ||
    6.51 -        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
    6.52 -      Scan.optional Parse_Spec.includes [] --
    6.53 -      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
    6.54 -        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    6.55 -          Thm.theoremK NONE (K I) a includes elems concl)));
    6.56 -
    6.57 -val _ = theorem @{command_keyword theorem} false "theorem";
    6.58 -val _ = theorem @{command_keyword lemma} false "lemma";
    6.59 -val _ = theorem @{command_keyword corollary} false "corollary";
    6.60 -val _ = theorem @{command_keyword proposition} false "proposition";
    6.61 -val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
    6.62 -
    6.63 -
    6.64  val _ =
    6.65    Outer_Syntax.command @{command_keyword have} "state local goal"
    6.66      (structured_statement >> (fn (a, b, c, d) =>