How to fix "partially applied constant on left hand side of code equation"?

I'm trying to define the code equation:

datatype t = A | B | C

inductive less_t :: "t ⇒ t ⇒ bool" where
  "less_t A B"
| "less_t B C"

code_pred [show_modes] less_t .

fun less_t_fun :: "t ⇒ t ⇒ bool" where
  "less_t_fun A A = False"
| "less_t_fun A B = True"
| "less_t_fun A C = True"
| "less_t_fun B C = True"
| "less_t_fun B _ = False"
| "less_t_fun C _ = False"

lemma tancl_less_t_code [code]:
  "less_t⇧+⇧+ x y ⟷ less_t_fun x y"
  apply (rule iffI)
  apply (erule tranclp_trans_induct)
  apply (erule less_t.cases; simp)
  apply (metis less_t_fun.elims(2) less_t_fun.simps(3) t.simps(4))
  apply (induct rule: less_t_fun.induct; simp)
  using less_t.intros apply auto
  done

value "less_t A B"
value "less_t_fun A C"
value "less_t⇧+⇧+ A C"

And get the following warning:

Partially applied constant "less_t" on left hand side of equation, in theorem:
less_t⇧+⇧+ ?x ?y ≡ less_t_fun ?x ?y

This question is unrelated to transitive closures. I already received such a warning for different theorems:

I just need to understand the meaning of this warning and how to fix it. Maybe I should define a different lemma?

Solution

The problem is that the structure of your lemma tancl_less_t_code is indeed not suitable as code-equations. Note that the outermost constant in the left-hand side of the equations is the transitive closure predicate tranclp. So, this tells the code-generator to use the lemma in order to implement tranclp. However, using your lemma one only knows how to implement tranclp for one specific predicate, namely less_t. Therefore, you get the complaint from Isabelle that your implementation is too specific.

There are at least two workarounds.

First, instead of the declaration [code], you can use [code unfold]. Then every occurrence of tranclp less_t x y will be replaced by less_t_fun during the code generation. To make this rule even more applicable, I would then reformulate the lemma to tranclp less = less_t_fun, so that even if tranclp less_t is not fully applied, the unfolding can happen.

Second, you can take the symmetric version of your lemma and declare it as [simp]. Then in your implementation you just invoke less_t_fun instead of tranclp less_t and in the proofs the simplifier will switch to the latter one.

For more information on [code] and [code_unfold] have a look into the documentation of the code generator.