假设我有一个二元运算符f :: "sT => sT => sT"。我想定义f它为克莱因四组实现一个 4x4 乘法表，在 Wiki 上显示：
http://en.wikipedia.org/wiki/Klein_four-group
在这里，我要做的就是创建一个包含 16 个条目的表。首先，我定义了四个这样的常量：
consts
k_1::sT
k_a::sT
k_b::sT
k_ab::sT
然后我定义我的函数来实现表中的 16 个条目：
k_1 * k_1 = k_1
k_1 * k_a = k_a
...
k_ab * k_ab = k_1
我不知道如何在 Isar 中进行任何类似普通的编程，并且我在 Isabelle 用户的列表中看到，据说（某些）类似编程的结构在语言中被有意淡化了。
前几天，我试图创建一个简单的、人为的函数，在找到if, then, else源文件中的使用后，我在isar-ref.pdf中找不到对这些命令的引用。
在查看教程时，我看到definition了以一种直接的方式定义函数，除此之外，我只看到有关递归和归纳函数的信息，它们需要datatype，而我的情况比这更简单。
如果留给我自己的设备，我想我会尝试datatype为上面显示的这 4 个常量定义 a，然后创建一些转换函数，以便最终得到一个二元运算符f :: sT => sT => sT。我在尝试使用时有点搞砸了fun，但这并不是一件简单的事情。
我做了一些fun实验inductive
更新：我在这里添加了一些材料来回应评论告诉我编程和证明是我可以找到答案的地方。看来我可能会误入理想的 Stackoverflow 格式。
我做了一些基本的实验，主要是用fun，但也用inductive. 我很快就放弃了归纳法。这是我从简单示例中得到的错误类型：
consts
k1::sT
inductive k4gI :: "sT => sT => sT" where
"k4gI k1 k1 = k1"
--"OUTPUT ERROR:"
--{*Proofs for inductive predicate(s) "k4gI"
Ill-formed introduction rule ""
((k4gI k1 k1) = k1)
Conclusion of introduction rule must be an inductive predicate
*}
我的乘法表不是归纳法，所以我不认为这inductive是我应该花时间去追求的。
“模式匹配”在这里似乎是一个关键思想，所以我尝试了fun. 这是一些试图fun仅与标准函数类型一起使用的非常混乱的代码：
consts
k1::sT
fun k4gF :: "sT => sT => sT" where
"k4gF k1 k1 = k1"
--"OUTPUT ERROR:"
--"Malformed definition:
Non-constructor pattern not allowed in sequential mode.
((k4gF k1 k1) = k1)"
我遇到了这种错误，我在Programming and Proving中读过这样的内容：
“递归函数是通过对数据类型构造函数进行模式匹配来有趣地定义的。
fun这一切都给新手一个需要的印象datatype。至于它的大哥function，我不知道。
似乎在这里，我需要的只是一个具有 16 个基本情况的递归函数，这将定义我的乘法表。
是function答案吗？
在编辑这个问题时，我想起function了过去，这是function在工作：
consts
k1::sT
function k4gF :: "sT => sT => sT" where
"k4gF k1 k1 = k1"
try
try 的输出告诉我它可以被证明（更新：我认为它实际上告诉我只有 1 个证明步骤可以被证明。）：
Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"...
Timestamp: 00:47:27.
solve_direct: (((k1, k1) = (k1, k1)) ⟹ (k1 = k1)) can be solved directly with
HOL.arg_cong: ((?x = ?y) ⟹ ((?f ?x) = (?f ?y))) [name "HOL.arg_cong", kind "lemma"]
HOL.refl: (?t = ?t) [name "HOL.refl"]
MFZ.HOL⇣'eq⇣'is⇣'reflexive: (?r = ?r) [name "MFZ.HOL⇣'eq⇣'is⇣'reflexive", kind "theorem"]
MFZ.HOL_eq_is_reflexive: (?r = ?r) [name "MFZ.HOL_eq_is_reflexive", kind "lemma"]
Product_Type.Pair_inject:
(⟦((?a, ?b) = (?a', ?b')); (⟦(?a = ?a'); (?b = ?b')⟧ ⟹ ?R)⟧ ⟹ ?R)
[name "Product_Type.Pair_inject", kind "lemma"]
我不知道那是什么意思。我只知道function因为试图证明不一致。我只知道它没有抱怨那么多。如果function像这样使用是我定义乘法表的方式，那么我很高兴。
尽管如此，作为一个争论的类型，我没有function在教程中学习。几个月前我在参考手册中了解到它，但我仍然不太了解如何使用它。
我有一个function我用 证明的auto，但幸运的是，这个功能可能不好。这增加了function的神秘感。function在 Isabelle/HOL中定义递归函数中有关于的信息，它比较fun和function。
但是，我还没有看到funorfunction不使用递归数据类型的示例，例如nator 'a list。可能我看的不够仔细。
抱歉，这很冗长，这不是一个直接的问题，但是没有伊莎贝尔的教程可以将一个人直接从 A 带到 B。