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

Question

所以我想定义一个函数(我们将其称为applied)，它将消除另一个multiset中子multiset的所有出现，并将每个出现替换为单个元素。例如,

applied {#a,a,c,a,a,c#} ({#a,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,a,c,a,a,c#} ({#a,a,c#}, f) = {#f,a,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...*)

不幸的是，我似乎无法证明这个函数的终止。我试过使用"termination" auto, fastforce, force等，甚至是大锤，但我似乎找不到这个函数工作的证据。

我可以得到一些帮助来解决这个问题吗?

Answer 1

像这样递归地定义它确实有点棘手，因为不能保证终止。如果是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)"

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