如何证明一个函数在其域上是完全的？

Question

我有以下理论：

theory Color 
imports Main 

begin 

datatype color = RED | GREEN 

function invert :: "color => color" 
where 
  "invert RED   = GREEN" 
| "invert GREEN = RED  " 
apply (pat_completeness) 
apply auto 
done 
termination by lexicographic_order 

lemma invert_univ: "invert_dom = (λx. True)" 

我想证明invert在其整个域中是完全的，因此invert_dom定义了数据类型color上的通用集。如何处理这个证据？或者，我应该用其他方法来表述这个问题吗？

Answer 1

首先，这里真的不需要使用function。此函数的终止证明很简单，可以自动找到，因此您只需编写

fun invert :: "color ⇒ color" 
where 
  "invert RED   = GREEN" 
| "invert GREEN = RED"

或者，因为它是在数据类型color上原始递归的。

primrec invert :: "color ⇒ color" 
where 
  "invert RED   = GREEN" 
| "invert GREEN = RED"

甚至只是

definition invert :: "color ⇒ color" where
  "invert c = (case c of RED ⇒ GREEN | GREEN ⇒ RED)"

在最后一种情况下，您必须使用引理invert invert_def手动展开对invert_def的定义。

现在来问你的实际问题:在技术上，在HOL中，每个功能都是全部的。这是必然的，因为在逻辑中，表达式根本没有价值的逻辑往往变得非常混乱。您可以通过对某些输入返回undefined来“模拟”非全局性，这是一些您不知道的任意值。undefined :: int是一些整数值--它可以是0，也可以是42或任何其他整数。对于用函数包定义的函数，只有在不指定情况(例如，不给出一个情况的等式)或函数没有终止于某些输入(然后就会变得混乱；如果您想对函数进行任何推理时，必须证明它在您首先给出的输入上终止)，这才是相关的。

如果您已经给出了终止证明--在本例中，由于函数微不足道地终止-- invert_dom谓词基本上是无用的。你不需要它。

否则，您可以使用invert_dom规则证明invert.domintros保持给定的输入。由于在实践中很少需要它们，所以您必须手动打开它们的生成，使用function (domintros)而不是function。这样你就可以证明你建议的引理：

lemma "invert_dom = (λ_. True)"
proof
  fix x show "invert_dom x = True"
    by (cases x) (auto intro: invert.domintros)
qed

但是，同样，*_dom谓词在实践中很少使用。