在 Isar 中定义有限乘法表的好方法是什么？

Question

假设我有一个二元运算符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，而我的情况比那个。

如果留给我自己的设备，我想我会尝试为上面显示的这 4 个常量定义一个 datatype，然后创建一些转换函数，以便最终得到一个二元运算符 f :: sT => sT => sT。我在尝试使用 fun 时有点搞砸了，但这并不是一件简单的事情。

我对@9​​87654338@ 和inductive 做了一些试验

更新：我在这里添加了一些材料来回应评论告诉我Programming and Proving 是我可以找到答案的地方。看来我可能会误入理想的 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通过数据类型构造函数的模式匹配来定义的。

这一切都让新手觉得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 的神秘感。 Defining Recursive Functions in Isabelle/HOL中有function的信息，比较fun和function。

但是，我还没有看到不使用递归数据类型的fun 或function 示例，例如nat 或'a list。也许我看起来不够努力。

很抱歉，这不是一个直接的问题，但没有任何关于 Isabelle 的教程可以将一个人直接从 A 带到 B。

Answer 1

下面，我不坚持“只回答问题”的格式，而是回答我自己的问题，所以我所说的一切都会引起原始发帖人的兴趣。

（第二次更新开始）

这应该是我最后一次更新了。要满足于“简单的方法”，能够进行比较以了解“低技术”的方法可能是最好的方法是有帮助的。

我终于放弃尝试让我的主要类型与新类型一起使用，我只是像这样从datatype 中让我成为克莱因四组，其中关联性的证明在最后：

datatype AT4k = e4kt | a4kt | b4kt | c4kt  

fun AOP4k :: "AT4k => AT4k => AT4k" where
  "AOP4k e4kt y    = y"
| "AOP4k x    e4kt = x"
| "AOP4k a4kt a4kt = e4kt"
| "AOP4k a4kt b4kt = c4kt"
| "AOP4k a4kt c4kt = b4kt"
| "AOP4k b4kt a4kt = c4kt"
| "AOP4k b4kt b4kt = e4kt"
| "AOP4k b4kt c4kt = a4kt"
| "AOP4k c4kt a4kt = b4kt"
| "AOP4k c4kt b4kt = a4kt"
| "AOP4k c4kt c4kt = e4kt"

notation
  AOP4k ("AOP4k") and
  AOP4k (infixl "*" 70) 

theorem k4o_assoc2:
  "(x * y) * z = x * (y * z)"
by(smt AOP4k.simps(1) AOP4k.simps(10) AOP4k.simps(11) AOP4k.simps(12) 
  AOP4k.simps(13) AOP4k.simps(2) AOP4k.simps(3) AOP4k.simps(4) AOP4k.simps(5) 
  AOP4k.simps(6) AOP4k.simps(7) AOP4k.simps(8) AOP4k.simps(9) AT4k.exhaust)

结果是我现在满足于我的if-then-else 乘法函数。为什么？因为if-then-else函数非常有利于simp变魔术。这种模式匹配本身并没有任何魔力，更不用说我仍然需要解决它的强制子类型部分。

这是 4x4 乘法表的 if-then-else 函数：

definition AO4k :: "sT => sT => sT" where
  "AO4k x y = 
    (if x = e4k then y   else
    (if y = e4k then x   else
    (if x = y   then e4k else
    (if x = a4k  y = c4k then b4k else
    (if x = b4k  y = c4k then a4k else
    (if x = c4k  y = a4k then b4k else  
    (if x = c4k  y = b4k then a4k else 
            c4k)))))))"

由于嵌套的if-then-else 语句，当我运行auto 时，它会产生64 个目标。我制定了 16 条 simp 规则，乘法表中的每个值一个，所以当我运行 auto 时，使用所有其他 simp 规则，auto 证明大约需要 90 毫秒。

低技术有时是要走的路；这是 RISC 与 CISC 的事情，有点。

像乘法表这样的小东西对于测试事物可能很重要，但如果它会减慢我的速度，它就没有用处了，因为它处于一个需要永远完成的大循环中。

（第二次更新结束）

（更新开始）

（更新：我上面的问题属于“我如何在 Isabelle 中进行基本编程，就像使用其他编程语言一样？”在这里，我超出了一些具体问题，但我尽量让我的 cmets 了解挑战对于在文档处于中级水平时尝试学习 Isabelle 的初学者，至少在我看来是这样。

不过，具体到我的问题是，我需要一个 case 语句，这是许多编程语言的一个非常基本的特性。

今天在寻找case 声明时，我认为我在文档中再搜索一次后找到了黄金，这次是Isabelle - A Proof Assistant for Higher-Order Logic。

在第 5 页上记录了 case 声明，但在第 18 页上，它澄清了它只对 datatype 有用，我似乎确认了这样的错误：

definition k4oC :: "kT => kT => kT" (infixl "**" 70) where
  "k4oC x y = (case x y of k1 k1 => k1)"
--{*Error in case expression:
    Not a datatype constructor: "i130429a.k1"
    In clause
    ((k1 k1) ⇒ k1)*}

这是一个例子，无论是专家还是初学者，都需要一个教程来运行 Isabelle 的基本编程功能。

如果您说，“有教程可以做到这一点。”我说，“不，没有，在我看来不是”。

这些教程强调了 Isabelle 的重要而复杂的特性，这些特性使它与众不同。

这是评论，但它的评论是为了与“我如何学习伊莎贝尔？”这个问题相关联，而我上面的原始问题与此相关。

如果您不是剑桥、TUM 或 NICTA 的博士研究生，那么您学习 Isabelle 的方式是，您需要挣扎 6 到 12 个月或更长时间。如果在那段时间里你没有放弃，你的水平可以让你欣赏可用的中级指导。经验可能会有所不同。

对我来说，当我有时间阅读它们时，这 3 本书将带我进入新的证明水平，让我摆脱 auto 和 metis，它们是

• Isabelle - A Proof Assistant for Higher-Order Logic
• Programming and Proving in Isabelle/HOL
• Isabelle/Isar --- a versatile environment for human-readable formal proof documents

如果有人说：“你滥用了 Stackoverflow 的答案格式，发表了冗长的评论和意见。”

我说，“好吧，我要求一种在 Isabelle 中进行基本编程的好方法，我希望在这种情况下，我希望得到比 if-then-else 大声明更复杂的东西。没有人提供任何接近我要求的东西。其实我是提供了模式匹配功能的人，我需要做的甚至还没有接近文档化。模式匹配是一个简单的概念，但在 Isabelle 中却不一定，因为递归函数的证明要求。（如果有一种简单的方法可以替换下面我的if-then-else 函数，甚至是case 语句方式，我很想知道。）

话虽如此，我还是有点冒昧，无论如何，目前这个页面只有 36 次浏览，其中可能至少有 10 次来自我的浏览器。

Isabelle/HOL 是一种强大的语言。我没有抱怨。只是听起来像。）

（更新结束）

仅仅知道某事是真还是假就很重要，在这种情况下，被告知function 可以与非归纳类型一起使用。但是，我最终如何使用下面的 function 并不是我在任何一份 Isabelle 文档中看到的任何结果，我需要这个关于强制子类型的前 SO 问题：

What is an Isabelle/HOL subtype? What Isar commands produce subtypes?

我最终有两种方法来完成乘法表的 2x2 部分。我在这里链接到理论：ASCII friendly A_i130429a.thy、jEdit friendly i130429a.thy、PDF 和 folder。

两种方式分别是：

1. 笨拙但快速且simp 友好if-then-else 的方式。定义耗时 0ms，证明耗时 155ms。
2. 使用function的模式匹配方式。在这里，我可以在公共场合大声思考这种做事方式很长一段时间，但我不会。我知道我会使用我在这里学到的东西，但是对于简单的乘法表函数来说，这绝对不是一个优雅的解决方案，而且很明显，一个人必须做所有这些来创建一个使用模式匹配的基本函数.当然，也许我不必做所有这些。定义耗时 391ms，证明耗时 317ms。

至于不得不求助于if-then-else，要么 Isabelle/HOL 在基本编程语句方面功能不丰富，要么这些基本语句没有记录。 if-then-else 语句甚至不在 Isar Reference Manual 索引中。我想，“如果没有记录，也许有一个很好的、没有记录的case 声明，比如Haskell has”。尽管如此，我还是会选择 Isabelle 而不是 Haskell。

下面，我解释 A_i130429a.thy 的不同部分。这有点微不足道，但并不完全，因为我还没有看到一个例子来教我如何做到这一点。

我从一个类型和四个未定义的常量开始。

typedecl kT
consts
  k1::kT
  ka::kT
  kb::kT
  kab::kT

值得注意的是，常量仍未定义。我留下了很多未定义的东西，这也是我在文档和资源中找不到好的示例以用作自己的模板的部分原因。

我做了一个测试，尝试在非归纳数据类型上智能地使用function，但它不起作用。使用我的if-then-else 函数，在我发现我没有限制我的函数域之后，我发现这个函数的问题也与域有关。 function k4f0 希望 x 成为 k1 或 ka 对于每个 x，这显然不是真的。

function k4f0 :: "kT => kT" where
  "k4f0 k1 = k1"
| "k4f0 ka = ka"
apply(auto)
apply(atomize_elim)
--"goal (1 subgoal):
   1. (!! (x::sT). ((x = k1) | (x = ka)))"

我放弃了，用if-then-else给我定义了一个丑陋的函数。

definition k4o :: "kT => kT => kT" (infixl "**" 70) where
  "k4o x y =
    (if x = k1 & y = k1 then k1 else
    (if x = k1 & y = ka then ka else
    (if x = ka & y = k1 then ka else
    (if x = ka & y = ka then k1 else (k1)
    ))))"
declare k4o_def [simp add]

困难的部分变成试图证明我的函数k4o 的关联性。但这只是因为我没有限制域。我在语句中添加了一个含义，auto 魔法开始了，fastforce 魔法也在那里，而且速度更快，所以我使用它。

abbreviation k4g :: "kT set" where
  "k4g == {k1, ka}"

theorem
  "(x \<in> k4g & y \<in> k4g & z \<in> k4g) --> (x ** y) ** z = x ** (y ** z)"
  by(fastforce)(*155ms*)

魔法让我很开心，然后我就有动力尝试使用function 和模式匹配来完成它。由于最近关于强制子类型的 SO 答案，链接到上面，我想出了如何使用typedef 修复域。我认为这不是完美的解决方案，但我确实学到了一些东西。

typedef kTD = "{x::kT. x = k1 | x = ka}"
  by(auto)
declare [[coercion_enabled]]
declare [[coercion Abs_kTD]]

function k4f :: "kTD => kTD => kT" (infixl "***" 70) where
  "k4f k1 k1 = k1"
| "k4f k1 ka = ka"
| "k4f ka k1 = ka"
| "k4f ka ka = k1"
by((auto),(*391ms*)
  (atomize_elim),
  (metis (lifting, full_types) Abs_kTD_cases mem_Collect_eq),
  (metis (lifting, full_types) Rep_kTD_cases Rep_kTD_inverse mem_Collect_eq),
  (metis (lifting, full_types) Rep_kTD_cases Rep_kTD_inverse mem_Collect_eq),
  (metis (lifting, full_types) Rep_kTD_cases Rep_kTD_inverse mem_Collect_eq),
  (metis (lifting, full_types) Rep_kTD_cases Rep_kTD_inverse mem_Collect_eq))
termination
by(metis "termination" wf_measure)

theorem
  "(x *** y) *** z = x *** (y *** z)"
by(smt
  Abs_kTD_cases
  k4f.simps(1)
  k4f.simps(2)
  k4f.simps(3)
  k4f.simps(4)
  mem_Collect_eq)(*317ms*)

Answer 2

定义“有限”函数的一种或多或少方便的语法是函数更新语法：对于函数f，f(x := y) 表示函数%z. if z = x then y else f z。如果要更新多个值，请用逗号分隔它们：f(x1 := y1, x2 := y2)。

因此，例如 0、1 和 undefined else 的加法函数可以写成：

undefined (0 := undefined(0 := 0, 1 := 1),
           1 := undefined(0 := 1, 1 := 2))

定义有限函数的另一种可能性是从对列表中生成它；例如map_of。使用f xs y z = the (map_of xs (y,z))，那么上面的函数可以写成

f [((0,0),0), ((0,1),1), ((1,0),1), ((1,1),1)]

（实际上，它并不是完全相同的函数，因为它可能在定义的域之外表现不同）。