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

Question

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

它接受一个函数 C，可以将 'a multiset 转换为 'a 类型的单个元素。这里我们假设 C 域中的每个元素都是成对互斥的，而不是空的多重集（我已经有另一个函数来检查这些东西）。 apply 还将采用另一个多重集 inp。我希望函数做的是检查 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

想多了，我不相信有一个简单的解决方案可以解决那个伊莎贝尔。

你需要吗？

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

如何表达定义？

我会使用一个归纳谓词来表达一个重写步骤并证明解决方案是唯一的。一些东西：

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 域中 subseqs 中的第一个元素重写。只要有任何可能的重写就进行迭代。

Link 归纳谓词证明终止并计算正确的东西。

请注意，通常您不能从多重集中提取列表，但在某些情况下可以这样做（例如，如果您对 'a 有 linorder）。

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

How can I subtract a multiset from a set with a given multiset?

set

logic

isabelle

multiset

你需要吗？

如何表达定义？

如何执行