Is it possible to add assumptions to the domain of a function in Isabelle?

Question

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!

Answer 1

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.

Answer 2

If your only problem with the non-recursive definition is how to apply it to concrete inputs, I still think the alternative definition that I said was executable is the way to go. Here's a prove that the two non-recursive definitions I gave are equivalent, and the application to the example you gave above:

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

lemma count_le_size: "count M x ≤ size M"
  by (induction M) auto

lemma applied_code [code]:
  "applied ms xs y = (if xs = {#} then ms else
     (let n = (MIN x ∈set_mset xs. count ms x div count xs x)
      in ms - repeat_mset n xs + replicate_mset n y))"
  unfolding applied_def
proof (intro if_cong let_cong refl)
  assume ne: "xs ≠ {#}"
  have subset: "{n. repeat_mset n xs ⊆# ms} ⊆ {..size ms}"
  proof safe
    fix n assume n: "repeat_mset n xs ⊆# ms"
    from ne obtain x where x: "x ∈# xs"
      by auto
    have "n * 1 ≤ n * count xs x"
      using x by (intro mult_left_mono) auto
    also have "… = count (repeat_mset n xs) x"
      by simp
    also have "… ≤ count ms x"
      using n by (intro mset_subset_eq_count)
    also have "… ≤ size ms"
      by (rule count_le_size)
    finally show "n ≤ size ms" by simp
  qed
  hence finite: "finite {n. repeat_mset n xs ⊆# ms}"
    by (rule finite_subset) auto

  show "Max {n. repeat_mset n xs ⊆# ms} = (MIN x∈set_mset xs. count ms x div count xs x)"
  proof (intro antisym)
    show "Max {n. repeat_mset n xs ⊆# ms} ≤ (MIN x∈set_mset xs. count ms x div count xs x)"
    proof (rule Max.boundedI)
      show "{n. repeat_mset n xs ⊆# ms} ≠ {}"
        by (auto intro: exI[of _ 0])
    next
      fix n assume n: "n ∈ {n. repeat_mset n xs ⊆# ms}"
      show "n ≤ (MIN x∈set_mset xs. count ms x div count xs x)"
      proof (safe intro!: Min.boundedI)
        fix x assume x: "x ∈# xs"
        have "count (repeat_mset n xs) x ≤ count ms x"
          using n by (intro mset_subset_eq_count) auto
        also have "count (repeat_mset n xs) x = n * count xs x"
          by simp
        finally show "n ≤ count ms x div count xs x"
          by (metis count_eq_zero_iff div_le_mono nonzero_mult_div_cancel_right x)
      qed (use ne in auto)
    qed (fact finite)
  next
    define m where "m = (MIN x∈set_mset xs. count ms x div count xs x)"
    show "m ≤ Max {n. repeat_mset n xs ⊆# ms}"
    proof (rule Max.coboundedI[OF finite], safe)
      show "repeat_mset m xs ⊆# ms"
      proof (rule mset_subset_eqI)
        fix x
        show "count (repeat_mset m xs) x ≤ count ms x"
        proof (cases "x ∈# xs")
          case True
          have "count (repeat_mset m xs) x = m * count xs x"
            by simp
          also have "… ≤ (count ms x div count xs x) * count xs x"
            unfolding m_def using ‹x ∈# xs› by (intro mult_right_mono Min.coboundedI) auto
          also have "… ≤ count ms x"
            by simp
          finally show ?thesis .
        next
          case False
          hence "count xs x = 0"
            by (meson not_in_iff)
          thus ?thesis by simp
        qed
      qed
    qed
  qed
qed

lemma replicate_mset_unfold:
  assumes "n > 0"
  shows   "replicate_mset n x = {#x#} + replicate_mset (n - 1) x"
  using assms by (cases n) auto

lemma
  assumes "a ≠ c" "a ≠ f" "c ≠ f"
  shows   "applied {#a,a,c,a,a,c#} {#a,a,c#} f = mset [f, f]"
  using assms
  by (simp add: applied_code replicate_mset_unfold flip: One_nat_def)

The value command does not work on that example because a, c, etc. are free variables. But if you e.g. make an ad-hoc datatype for them, it works:

datatype test = a | b | c | f

value "applied {#a,a,c,a,a,c#} {#a,a,c#} f"
(* "mset [f, f]" :: "test multiset" *)