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

编程问答 2022-05-27

问题描述

因此，我想定义一个函数（我们将其称为 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 等，甚至是大锤，但我似乎找不到这个功能工作的证据。

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

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

functionfunctionisabellemultisetproof