如何在Isabelle/HOL中为Isar的lemma添加example同义词？

你可以通过Isabelle的ML扩展机制，轻松将example定义为与无名lemma完全等价的命令，配置方法简单且稳定：

1. 在理论文件开头添加以下ML代码，注册example命令：

ML ‹
  Outer_Syntax.command @{command_keyword "example"} "example (anonymous lemma)"
    (Parse_Spec.opt_thm_name ":" -- Parse_Spec.prop -- Parse.for_fixes >>
      (fn ((_, prop), fixes) =>
        Toplevel.theory (Spec.add_anonymous_lemma NONE fixes prop)))
›

这段代码直接复用了无名lemma的底层实现逻辑，确保example和无名称的lemma行为完全一致，包括支持命题、变量绑定以及后续的证明方法。

2. 之后就可以按你期望的方式编写代码：

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

example "foo_function 3 = 4" by eval

稳定性说明 #

该配置基于Isabelle官方提供的Outer_Syntax和Spec接口，属于标准扩展方式。这类核心语法接口在Isabelle的版本迭代中通常保持向后兼容，因此配置可以长期稳定使用。若要全局生效，可将上述ML代码添加到~/.isabelle/etc/settings或自定义会话配置文件中，无需在每个理论文件重复添加。

内容的提问来源于stack exchange，提问作者corny