问题描述
所以我试图定义一个函数 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)。