如何定义具有重叠模式的函数？

Question

我正在尝试为 4 值逻辑（假、真、空和错误）定义一个合取函数：

datatype 'a maybe = Just "'a" | Nothing | Error
type_synonym bool4 = "bool maybe"

abbreviation JF :: "bool4" where "JF ≡ Just False"
abbreviation JT :: "bool4" where "JT ≡ Just True"
abbreviation BN :: "bool4" where "BN ≡ Nothing"
abbreviation BE :: "bool4" where "BE ≡ Error"

fun and4 :: "bool4 ⇒ bool4 ⇒ bool4" where
  "and4 JF b = JF"
| "and4 a JF = JF"
| "and4 BE b = BE"
| "and4 a BE = BE"
| "and4 BN b = BN"
| "and4 a BN = BN"
| "and4 a b  = JT"

我希望第一个模式优先于最后一个模式。

好像定义有误。我正在尝试评估以下表达式：

value "and4 JF b"
value "and4 a JF"

第一个returnsJF果然如此。但是第二个不能简化。

因此我无法证明合取的交换律:

lemma and4_commut:
  "and4 a b = and4 b a"

建议在"Defining Recursive Functions in Isabelle/HOL" by Alexander Krauss中使用function代替fun。但是我得到了 12 个错误的子目标：

function and4 :: "bool4 ⇒ bool4 ⇒ bool4" where
  "and4 JF b = JF"
| "and4 a JF = JF"
| "and4 BE b = BE"
| "and4 a BE = BE"
| "and4 BN b = BN"
| "and4 a BN = BN"
| "and4 a b  = JT"
  apply pat_completeness
  apply auto

我猜是因为函数有冲突的模式。例如，and4 JF BE 匹配第一个和第四个模式。连词结果可以是JF也可以是BE。

定义此类函数的正确方法是什么？以及如何证明它的交换性？我可以使用 case of 构造，但它会使函数定义复杂化。

Answer 1

value命令通常不能很好地处理自由变量（如a）。

但是，您可以通过区分大小写来证明定理 FooAndValue a JF = JF：

lemma and4_JF_right [simp]: "and4 a JF = JF"
proof (cases a)
  case (Just b)
  thus ?thesis by (cases b) simp_all
qed simp_all

或者，更简洁一些，使用自定义 case 规则：

lemma bool4_cases [case_names JF JT BN BE]: 
  "(a = JF ⟹ P) ⟹ (a = JT ⟹ P) ⟹ (a = BN ⟹ P) ⟹ (a = BE ⟹ P) ⟹ P"
  by (cases a) auto

lemma and4_JF_right [simp]: "and4 a JF = JF"
  by (cases a rule: bool4_cases) simp_all

有了这个，证明交换性可以通过一行简单的归纳来完成。

为什么 fun 命令没有给你 and4 a JF = JF 作为定理，即使你在定义中确实写了它是因为你确实有重叠模式并使用顺序模式匹配，即函数定义中的第二个“等式”仅在第一个不适用时适用。

fun 必须解决重叠模式以适应这种顺序匹配，在此之后，and4 a JF = JF 成立并不明显（通常）。您可以查看 and4.simps 以确切了解 fun 做了什么。

如果我没记错的话，你也可以使用普通 function 来得到重叠模式 而无需 顺序匹配，但是你必须证明重叠方程是兼容的.对于您的情况，我认为这不会让事情变得更容易。

您可以做的另一件事（这可能更容易使用，具体取决于您的用例）是不使用 bool maybe，而是定义一个 4 构造函数数据类型并定义一个线性排序该类型，其中 JF < BE < BN < JT，然后 and4 相当于 min.

如何定义具有重叠模式的函数？

How to define functions with overlapping patterns?

isabelle