I'm not sure if it's okay to post a follow-up question like this, but I'll do it anyway.
So a few days ago I posted this question: How can I remove all occurrences of a sub-multiset in Isabelle?
I thought the answer was great, but when trying to prove the lemma
lemma "applied1 {#''a'',''a'',''d'',''c'',''a'',''a'',''d'',''c''#} {#''a'',''a'',''c''#} ''f'' = {#''f'',''f'',''d'',''d''#}"
I got really stuck. I found that I couldn't simply do it after unfolding the def and applying some simple automations. So I went back to my original function and made some tweaks to it such that it returns nothing if the input were to result in an infinite loop. I thought it was going to work this time, but Isabelle still couldn't prove termination. I'm pretty sure it's obvious that size x is constantly decreasing by a factor of size y and cannot be negative, so it will have to ultimately terminate when size x = 0 or when y is no longer a subset of x.
fun applied2 :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset option" where
"applied2 x y z = (if z ∈# y ∨ y = {#} then None else (if y ⊆# x then Some (plus {#z#} (the (applied2 (x - y) y z))) else Some x))"
Is it possible to convince Isabelle that this function terminates using function instead of fun? Or are there other constraints I have to take into account?
I'm really sorry if I shouldn't be posting questions like this. I'm still inexperienced with Isabelle and I do hope I'm upholding my purpose to learn about the language as best as I can. Thanks in advance!
I believe that looking at the documentation would have given you the correct syntax.
function applied2 :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset option" where
"applied2 x y z = (if z ∈# y ∨ y = {#} then None else (if y ⊆# x then Some (plus {#z#} (the (applied2 (x - y) y z))) else Some x))"
by pat_completeness auto
termination
by (relation "measure (λ(x,y,z). size x)")
(auto simp: mset_subset_eq_exists_conv nonempty_has_size)
If the problem is the proof, sledgehammer would have found it for you.
However, I don't see how you intend to go from applied2 to the function you really want. The real problem is determinism: you need an order to look at the subsets. Manuel's solution was using Sup, but this is indeed not executable.