How to define a partial function in Isabelle?

Question

I tried to define a partial function with the partial_function keyword. It did not work. Here is the one that expresses the intuition best:

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity Zero = Zero "
| "oddity (Succ (Succ n)) = n"

and then I tried the following:

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity arg = ( case arg of (Succ (Succ n)) => n
                          | Zero => Zero
                )"

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity (Succ(Succ n)) = n
   | oddity Zero = Zero"

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity n =
   (if n = Zero then Zero
    else if (n >= 2)
      then do { m ← oddity (n-2); m })"

None of them worked. I guess my attempts have conceptual and syntactic problems, what are these?

Answer 1

There are two problems with your definitions:

1. partial_function does not support pattern-matching on the left hand side. This must be emulated with case expressions on the right.

2. The constructors for type nat are Suc and 0, not Succ and Zero. This is why your case expressions generate the error that Succ and Zero are not datatype constructors, and why parital_function complains that Zero is an extra variable on the right hand side.

In summary, the following works:

partial_function (tailrec) oddity :: "nat => nat"
where "oddity arg = (case arg of (Suc (Suc n)) => n | 0 => 0 )"

You can recover simplification rules with pattern-matching by using the simp_of_case conversion from ~~/src/HOL/Library/Simps_Case_Conv:

simps_of_case oddity_simps[simp]: oddity.simps

thm oddity_simps