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  

Unfortunately, when I tried proving the lemma

lemma "applied {#''a'',''a'', ''a'',''a'',''c'',''c''#} ({#''a'',''a'',''c''#}, ''f'') = {#''f'',''f''#}"  

None of the proof methods off the top of my head would work (auto, simp, clarsimp, blast, force, fastforce, etc) because they couldn't be applied. Sledgehammer even timed out (I set it to run for 60 seconds instead of the default 30.)

Could I please have some help with this problem?

https://stackoverflow.com/questions/66057437/how-can-i-remove-all-occurrences-of-a-sub-multiset-in-isabelle February 05, 2021 at 12:06PM