关于Isabelle/HOL中thy_goal_defn、keywords及理论级定义的技术问询

我来帮你拆解这两个困惑点——Isabelle里keywords的工作逻辑，以及“理论级定义”到底指什么，结合你看到的Quotient.thy代码和手册内容来解释：

一、Isabelle中keywords的工作机制 #

Isabelle/Isar的命令语言是可扩展的，keywords声明本质上是在给Isabelle的语法解析器“提前打招呼”：接下来我要定义一些新的顶层命令或语法标记，你得识别它们，并且知道它们在证明文档的结构里扮演什么角色。

你看到的这段代码：

keywords "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and "quotient_type" :: thy_goal_defn and "/" and "quotient_definition" :: thy_goal_defn begin

可以拆成几个部分理解：

• "print_quotmapsQ3"等三个命令被归类为diag：这是诊断命令的范畴，这类命令用来输出理论内部的调试/信息，比如查看已定义的商映射、商类型，类似Isabelle自带的print_theorems、print_types，都是帮你检查当前理论状态的工具。
• "quotient_type"和quotient_definition被归类为thy_goal_defn：这代表它们是需要生成证明目标的理论级定义命令。意思是当你用这些命令定义实体时，Isabelle会自动抛出需要你证明的“义务”（比如定义商类型时要证明关系是等价关系），只有完成这些证明，定义才会被正式纳入理论。
• 单独的"/"是语法标记：它是quotient_type命令的一部分语法，用来分隔底层类型表达式和等价关系，比如你看到的rat = "int * int" / partial: "ratrel"，这里的/就是告诉解析器：左边是用来构造商类型的原类型（整数对），右边是用来划分等价类的关系（ratrel）。

简单说，keywords就是给解析器做“语法预注册”，避免把后续出现的新命令当成语法错误，同时明确它们的语义类别，让Isabelle知道怎么处理这些命令的逻辑。

二、什么是“理论级定义”？ #

理论级定义（theory-level definitions）是相对于局部定义（比如证明过程中用define或let做的临时定义）而言的，指的是直接在.thy文件的顶层（不在proof块内部）定义的、会被**永久加入当前理论（以及所有依赖该理论的其他理论）**的实体——比如类型、常量、定理、公理等。

Isabelle会根据定义是否需要用户提供证明，把理论级定义分成不同类别，手册里的例子很直观：

• typedef :: thy_goal_defn：定义新类型时，必须证明原集合非空（否则这个类型就不存在），所以属于带证明目标的理论级定义。
• datatype :: thy_defn：定义代数数据类型时，Isabelle会自动验证构造函数的合法性（比如无歧义性），不需要用户额外证明，所以属于不带证明目标的理论级定义。

回到你看到的quotient_type，它属于thy_goal_defn，因为定义商类型时，你必须证明指定的关系是等价关系（自反、对称、传递），或者是符合要求的偏等价关系（比如partial:标记的场景）。只有完成这些证明义务，新的商类型（比如rat有理数类型）才会被正式加入HOL理论，后续的所有代码才能合法使用这个类型。

理论级定义的核心是：它们是理论的“永久组成部分”，不是临时的证明辅助工具，会被Isabelle的理论管理系统持久化，供其他理论直接引用。

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