How can I remove all occurrences of a sub-multiset in Isabelle?

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?

Solution

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.