我是一个刚刚开始习惯 Isabelle 的数学家，本来应该非常简单的事情结果却令人沮丧。如何定义两个常量之间的函数？比如说，函数 f: {1,2,3} \to {1,2,4} 映射 1 到 1、2 到 4 和 3 到 2？
我想我设法将集合定义为常量 t1 和 t2 没有意外，但是（我猜是因为它们不是数据类型）我不能尝试类似的东西
definition f ::"t1 => t2" where
"f 1 = 1" |
"f 2 = 4" |
"f 3 = 2"
我相信这个困难背后一定存在一个基本的误解，所以我感谢任何指导。
【问题讨论】：
标签： isabelle
您的问题有很多方面。
首先，要让某些东西快速运行，请使用 fun 关键字而不是 definition，如下所示：
fun test :: "nat ⇒ nat" where
"test (Suc 0) = 1" |
"test (Suc (Suc 0)) = 4" |
"test (Suc (Suc (Suc 0))) = 2" |
"test _ = undefined"
您不能使用definition 关键字直接在定义头部的任何参数上进行模式匹配，而您可以使用fun。另请注意，在模式匹配中，我已将重载的数字文字（1、2、3 等）替换为 nat 数据类型（0 和 Suc）的构造函数。
另一种方法是坚持使用definition，但使用case 语句将函数参数的案例分析推送到定义的主体中，如下所示：
definition test2 :: "nat ⇒ nat" where
"test2 x ≡
case x of
(Suc 0) ⇒ 1
| (Suc (Suc 0)) ⇒ 4
| (Suc (Suc (Suc 0))) ⇒ 2
| _ ⇒ undefined"
注意像test2这样的定义默认情况下不会被简化器展开，如果你想在证明中扩展test2的出现，你需要手动将定理test2_def添加到简化器的简化集中。
您还可以使用typedef 定义与您的两个三元素集相对应的新类型（您不能直接使用集合作为类型）typedef，但我个人会坚持使用nat。
编辑：要使用typedef，请执行以下操作：
typedef t1 = "{x::nat. x = 1 ∨ x = 2 ∨ x = 3}"
by auto
definition test :: "t1 ⇒ t1" where
"test x ≡
case (Rep_t1 x) of
| Suc 0 ⇒ Abs_t1 1
| Suc (Suc 0) ⇒ Abs_t1 4
| Suc (Suc (Suc 0)) ⇒ Abs_t1 2"
不过，我自己并没有真正使用过typedef，所以这可能不是使用它的最佳方式，其他人可能会建议其他方式。 typedef 所做的是通过为新类型识别一组非空的居民来从现有类型中开辟出一种新类型。证明义务，这里由auto 结束，只是为了证明新类型的定义集确实是非空的，在这种情况下，我正在将自然数的三元素集划分为一个新类型，称为t1，所以证明相当简单。创建了两个新常量Abs_t1 和Rep_t1，它们允许您在自然类型和新类型之间来回移动。如果你在typedef 命令后面加上print_theorems，你会看到Isabelle 自动为你生成的几个关于t1 的新定理。
【讨论】：
typedef：在你的情况下，它可能看起来像我上面的编辑。