How to resolve Isabelle termination _dom error message (avoiding recursive definition of two-argument max)?

Question

I am trying to define my own simple max function in Isabelle and prove its termination:

fun two_integer_max_case :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case a b = (case a > b of True ⇒ a | False ⇒ b)"

termination by auto

But there is un-handled goal in the termination proof:

proof (prove)
goal (1 subgoal):
 1. All two_integer_max_case_dom 
Ignoring duplicate rewrite rule:
two_integer_max_case ?a1 ?b1 ≡ case ?b1 < ?a1 of True ⇒ ?a1 | False ⇒ ?b1 
Duplicate fact declaration "Max_Of_Two_Integers.two_integer_max_case.simps" vs. "Max_Of_Two_Integers.two_integer_max_case.simps"⌂ 
Failed to finish proof⌂:
goal (1 subgoal):
 1. ⋀a b. two_integer_max_case_dom (a, b)

I am focused specifically on message:

Failed to finish proof⌂:
goal (1 subgoal):
1. ⋀a b. two_integer_max_case_dom (a, b)

What does it mean? What is required of me? This ..._dom condition. Where I can read about that?

I have read Chapters 3.5 of https://isabelle.in.tum.de/dist/Isabelle2021/doc/tutorial.pdf and now I am reading Chapter 8.1 of https://isabelle.in.tum.de/dist/Isabelle2021/doc/functions.pdf about domain predicates. Well, I hope that I manage find the solution.

I am aware that things would be easy (at least in the termination proof) if I had manage to come up with the recursive definition of my max function (two natural type arguments). But I have not managed to find such definition (I guess that there is some creative definition in the base theories already) and I am not sure whether I would be happy with recursive definition because my intention is to generate the Haskell or Scala code from this my function and I would prefer that this code would not be recursive but that it would use the standard less, equality operators of respective languages.

Well - it my be problem for the code synthesis with Isabelle generally - if Isabelle prefers recursive definitions of the algorithmic constructions for which industrial-programming-style (whatever it be) is not requiring recursion, then the generated code can be of less maintainability and human comprehension (still an issue before the AI has taken the field of program synthesis).

René Thiemann René Thiemann · Accepted Answer · 2021-03-20T18:46:20

There is no need to prove termination when using fun, since this Isabelle-command only accepts a function definition if it can prove termination automatically. Hence your termination-command is not necessary at all and actually confuses the system, since it has already proven termination.

Only when using function instead of fun, then you need to prove termination manually afterwards.

Hope this helps, René

How to resolve Isabelle termination _dom error message (avoiding recursive definition of two-argument max)?

1 Answers