如何删除Isabelle中所有出现的子多重集? [英] How can I remove all occurrences of a sub-multiset in Isabelle?

问题描述

因此，我想定义一个函数(我们称其为 applied )，该函数将消除另一个多重集中所有子多重集的所有出现，并用单个元素替换每次出现.例如，

应用了{#a，a，c，a，a，c#}({#a，a，c#}，f)= {#f，f#}

所以起初我尝试了一个定义:

 定义的应用:: :: [['a multiset，('a multiset×'a)]⇒'a multiset';在哪里应用的ms t =(如果(fst t)⊆#ms，然后加上(ms-(fst t)){#snd t#}否则ms)" 

但是，我很快意识到这只会删除该子集的一次出现.因此，如果我们通过前面的示例，我们将拥有

应用了{#a，a，c，a，a，c#}({#a，a，c#}，f)= {#f，a，a，c#}

这不理想.

然后我尝试使用一个函数(我最初尝试使用primrec，并且很有趣，但是前者不喜欢输入的结构，而fun不能证明该函数终止了.)

 函数的应用:: :: [['a multiset，('a multiset×'a)]⇒'a multiset';在哪里施加的ms t ＝(如果(fst t)≥#ms，然后施加(加上(ms-(fst t)){#snd t#})t else ms)"自动终止者(*不确定在此放置什么内容... *) 

不幸的是，我似乎无法证明该功能的终止.我尝试使用终止"，自动，fastforce，force等，甚至大锤，但我似乎找不到该功能正常工作的证据.

请问有关此问题的帮助吗?

解决方案

像这样递归地定义它确实有些棘手，因为不能保证终止.如果 fst t = {#snd t#} ，或更笼统地说 snd t∈#fst t ，该怎么办?然后，您的函数将继续运行，并且永不终止.

我认为，最简单的方法是进行一次性"替换的非递归定义:

 定义的:: ::多集⇒'多集⇒'a⇒'多集"在哪里应用的ms xs y =(让n = Inf((λx.count ms x div count xs x)`set_mset xs)以毫秒为单位-repeat_mset n xs +复制_mset n y)" 

我将元组参数更改为咖喱参数，因为根据我的经验，这在实践中更适用于证明–但是元组当然也可以工作.

n 是 xs 在 ms 中出现的次数.您可以通过检查其他函数的定义来查看它们的作用.

关于 n 的内容也可能会更明确一些，并这样写:

 定义的:: ::多集⇒'多集⇒'a⇒'多集"在哪里应用的ms xs y =(让n = Sup {n.repeat_msetn xs⊆#ms}以毫秒为单位-repeat_mset n xs +复制_mset n y)" 

缺点是此定义不再可执行-但两者应易于证明是等效的.

So I'd like to define a function (we'll call it applied) that would get rid of all occurrences of a sub-multiset within another multiset and replace each occurrence with a single element. For example,

applied {#a,a,c,a,a,c#} ({#a,a,c#}, f) = {#f,f#}

So at first I tried a definition:

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)"

However, I quickly realised that this would only remove one occurrence of the subset. So if we went by the previous example, we would have

applied {#a,a,c,a,a,c#} ({#a,a,c#}, f) = {#f,a,a,c#}

which is not ideal.

I then tried using a function (I initially tried primrec, and fun, but the former didn't like the structure of the inputs and fun couldn't prove that the function terminates.)

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...*)

Unfortunately, I can't seem to prove the termination of this function. I've tried using "termination", auto, fastforce, force, etc and even sledgehammer but I can't seem to find a proof for this function to work.

Could I please have some help with this problem?

解决方案

Defining it recursively like this is indeed a bit tricky because termination is not guaranteed. What if fst t = {# snd t #}, or more generally snd t ∈# fst t? Then your function keeps running in circles and never terminates.

The easiest way, in my opinion, would be a non-recursive definition that does a ‘one-off’ replacement:

definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
  "applied ms xs y =
     (let n = Inf ((λx. count ms x div count xs x) ` set_mset xs)
      in ms - repeat_mset n xs + replicate_mset n y)"

I changed the tupled argument to a curried one because this is more usable for proofs in practice, in my experience – but tupled would of course work as well.

n is the number of times that xs occurs in the ms. You can look at what the other functions do by inspecting their definitions.

One could also be a bit more explicit about n and write it like this:

definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
  "applied ms xs y =
     (let n = Sup {n. repeat_mset n xs ⊆# ms}
      in ms - repeat_mset n xs + replicate_mset n y)"

The drawback is that this definition is not executable anymore – but the two should be easy to prove equivalent.

这篇关于如何删除Isabelle中所有出现的子多重集?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！