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

所以我试图定义一个函数 public override void Execute(IRequest req,IResponse res,object requestDto) { req.QueryString.Add("foo","bar"); }

它接受一个函数 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)"

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

解决方法

经过深思熟虑后，我认为对于那个 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 为您提供所有可能的子集。使用 subseqs 中 C 域中的第一个元素重写。只要有任何可能的重写，就迭代。

将其链接到归纳谓词以证明终止并计算正确。

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