如何从具有给定多集的集合中减去多集

Question

所以我试图定义一个函数apply_C :: "('a multiset ⇒ 'a option) ⇒ 'a multiset ⇒ 'a multiset"

它采用函数C，该函数可以将'a multiset转换为类型为'a的单个元素。在这里，我们假设C的域中的每个元素是成对互斥的，而不是空的multiset(我已经有了另一个检查这些东西的函数(。CCD_ 6也将占用另一个多集CCD_。我想让函数检查C的域中是否至少有一个元素完全包含在inp中。如果是这种情况，则执行集合差inp - s，其中s是C的域中的元素，并将元素the (C s)添加到该结果多集合中。然后，继续运行该函数，直到C的域中不再有完全包含在给定inp多集中的元素。

我尝试了以下方法：

fun apply_C :: "('a multiset ⇒ 'a option) ⇒ 'a multiset ⇒ 'a multiset" where
"apply_C C inp = (if ∃s ∈ (domain C). s ⊆# inp then apply_C C (add_mset (the (C s)) (inp - s)) else inp)"

然而，我得到了这个错误：

Variable "s" occurs on right hand side only:
⋀C inp s.
apply_C C inp =
(if ∃s∈domain C. s ⊆# inp
then apply_C C
(add_mset (the (C s)) (inp - s))
else inp)

我已经考虑这个问题好几天了，还没能找到在Isabelle中实现这个功能的方法。我能帮忙吗？

Answer 1

仔细思考后，我认为没有简单的解决方案可以解决Isabelle。

你需要这个吗

我没有说你为什么要那样。也许你可以减少你的假设？你真的需要一个函数来计算结果吗？

如何表达定义

我会使用一个归纳谓词来表示重写的一个步骤，并证明解决方案是唯一的。大致情况：

context
fixes C :: ‹'a multiset ⇒ 'a option›
begin
inductive apply_CI where
‹apply_CI (M + M') (add_mset (the (C M)) M')›
if ‹M ∈ dom C›
context
assumes
distinct: ‹⋀a b. a ∈ dom C ⟹ b ∈ dom C ⟹ a ≠ b ⟹ a ∩# b = {#}› and
strictly_smaller: ‹⋀a b. a ∈ dom C ⟹ size a > 1› 
begin
lemma apply_CI_determ:
assumes
‹apply_CI⇧*⇧* M M⇩1› and
‹apply_CI⇧*⇧* M M⇩2› and
‹⋀M⇩3. ¬apply_CI M⇩1 M⇩3›
‹⋀M⇩3. ¬apply_CI M⇩2 M⇩3›
shows ‹M⇩1 = M⇩2›
sorry
lemma apply_CI_smaller:
‹apply_CI M M' ⟹ size M' ≤ size M›
apply (induction rule: apply_CI.induct)
subgoal for M M'
using strictly_smaller[of M]
by auto
done
lemma wf_apply_CI:
‹wf {(x, y). apply_CI y x}›
(*trivial but very annoying because not enough useful lemmas on wf*)
sorry
end
end

我不知道如何证明apply_CI_determ(不知道我写下的条件是否足够(，但我确实花了很多时间思考它

之后，你可以定义你的定义：

definition apply_C where
‹apply_C M = (SOME M'. apply_CI⇧*⇧* M M' ∧ (∀M⇩3. ¬apply_CI M' M⇩3))›

并在你的定义中证明属性。

如何执行

我不知道如何直接在多集上编写可执行函数。你面临的问题是apply_C的一个步骤是不确定的。

如果你可以使用列表而不是多集，你可以免费获得元素的顺序，你可以使用subseqs来提供所有可能的子集。使用C域中的子类中的第一个元素重写。只要有任何可能的重写，就迭代。

将其与归纳谓词联系起来，以证明终止，并证明它计算的是正确的。

请注意，通常情况下，您无法从多集合中提取列表，但在某些情况下可以这样做(例如，如果您在"a"上有一个linorder(。