添加“`example`”作为Isar‘`lemma`’的同义词

Question

在我的Isabelle/HOL理论中，我喜欢用未命名的引理作为例子。

下面是我的一些理论的例子。

definition foo_function :: "nat ⇒ nat" where "foo_function x = x+1"

text‹Example:›
lemma "foo_function 3 = 4" by eval

我觉得如果我有一个example关键字的话，整个理论会读得更好，这基本上相当于一个未命名的引理。以下是我想要写的：

definition foo_function :: "nat ⇒ nat" where "foo_function x = x+1"

example "foo_function 3 = 4" by eval

有一个超级简单和稳定的方式来设置这个吗？

Answer 1

控制-点击引理(除了证明，这是伊莎贝尔最重要的特点。真的。您可以控制-单击几乎所有的东西来了解它是如何定义的)并复制粘贴设置：

theory Scratch
  imports Main
  keywords "example" :: thy_goal_stmt
begin

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) Binding.empty_atts --
  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, Binding.empty_atts, [], [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>‹example› false "example";
in end
›
example True
  by eval
end