如何删除 Isabelle 中所有出现的子多重集？

如何解决如何删除 Isabelle 中所有出现的子多重集？

因此，我想定义一个函数（我们将其称为 applied），该函数将删除另一个多重集中出现的所有子多重集，并用单个元素替换每个出现。例如，

applied {#a,a,c,c#} ({#a,c#},f) = {#f,f#}

所以一开始我尝试了一个定义：

deFinition applied :: "['a multiset,('a multiset × 'a)] ⇒ 'a multiset" where
"applied ms t = (if (fst t) ⊆# ms then plus (ms - (fst t)) {#snd t#} else ms)"

然而，我很快意识到这只会删除一个子集。所以如果我们按照前面的例子，我们会有

applied {#a,c#}

这并不理想。

然后我尝试使用一个函数（我最初尝试过 primrec 和 fun，但前者不喜欢输入的结构，并且 fun 无法证明函数终止。）

function applied :: "['a multiset,('a multiset × 'a)] ⇒ 'a multiset" where
"applied ms t = (if (fst t) ⊆# ms then applied (plus (ms - (fst t)) {#snd t#}) t else ms)"
  by auto
termination by (*Not sure what to put here...*)

不幸的是，我似乎无法证明此功能的终止。我试过使用“终止”、自动、fastforce、force 等，甚至是大锤，但我似乎找不到这个功能工作的证据。

我能帮我解决这个问题吗？

解决方法

像这样递归定义它确实有点棘手，因为不能保证终止。如果 fst t = {# snd t #} 或更一般的 snd t ∈# fst t 会怎样？然后你的函数会一直循环运行，永不终止。

在我看来，最简单的方法是进行“一次性”替换的非递归定义：

definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
  "applied ms xs y =
     (let n = Inf ((λx. count ms x div count xs x) ` set_mset xs)
      in ms - repeat_mset n xs + replicate_mset n y)"

我将元组参数更改为柯里式参数，因为根据我的经验，这在实践中更适用于证明——但元组当然也能工作。

n 是 xs 在 ms 中出现的次数。您可以通过检查其他函数的定义来了解它们的作用。

关于 n 也可以更明确一点，写成这样：

definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
  "applied ms xs y =
     (let n = Sup {n. repeat_mset n xs ⊆# ms}
      in ms - repeat_mset n xs + replicate_mset n y)"

缺点是这个定义不再是可执行的——但是这两个应该很容易证明等价。