Isabelle theory 'Variable "return" occurs on right hand side only'

I am trying to create my first Isabelle/HOL theory for the algorithm, that computer max integer from the two integers. My intention is to formalize algorithms, this is the initial attempt. That is why I am trying to make my Isabelle code as similar to usual s. c. "industrial programming langauges" or the algol-style code as possible. So - no much use of the default primrec and recursive definitions (with matching and branching) that Isabelle prefers. I came up with the theory:

theory Max_Of_Two_Integers
  imports Main
begin

function two_integer_max :: "nat ⇒ nat ⇒ nat"
where
  "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second)"

end

But there is error message at function keyword:

Variable "return" occurs on right hand side only:
⋀first second return.
   two_integer_max first second =
   (if second < first then return first else return second)

I am closely following the pattern of very elaborate algorithm https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html and it used return as expected in usual programming.

So - what is wrong with my return command and how to correct it?

Besides, for this theory to be complete I have to prove termination (theorems about the nature of the function are not mandatory but I will add them).

Isabelle tutorial mainly uses primrec with recursive definition of functions and with pattern matching. I opted for function with the flexibility that comes with it (my guess).

Besides Tutorial, the blog post https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined is fantastic guide to functions for Isabelle - but it is strange - it does not provide the example with return keyword, although - as one can see in Imperative_Quicksort example, function and return are valid constructions.

Solution

The return is specific to writing imperative algorithms in Imperative HOL (which is what that Quicksort implementation is using). The same goes for the do notation. The reason why you get that error message is that you have not imported Imperative HOL.

Imperative HOL is essentially a library that allows you to write imperative programs that modify a heap. That's why the return type of quicksort in that example is not a list or an array, but a unit Heap. (But even if you had, you would still get an error message, since you are returning a nat and not a Heap).

If you're just starting out with Isabelle, I strongly recommend not to do anything with Imperative HOL for now. Rather, you should start with ‘normal’ Isabelle, which uses a functional style to define things. A good introduction into Isabelle is the first half of the Concrete Semantics book, which is available free online.