title: How to define a partial function in Isabelle?
body: <p>I tried to define a partial function with the <code>partial_function</code> keyword. It did not work. Here is the one that expresses the intuition best:</p>
  
  <pre><code>partial_function (tailrec) oddity :: "nat =&gt; nat"
  where
    "oddity Zero = Zero "
  | "oddity (Succ (Succ n)) = n"
  </code></pre>
  
  <p>and then I tried the following:</p>
  
  <pre><code>partial_function (tailrec) oddity :: "nat =&gt; nat"
  where
    "oddity arg = ( case arg of (Succ (Succ n)) =&gt; n
                            | Zero =&gt; Zero
                  )"
  
  partial_function (tailrec) oddity :: "nat =&gt; nat"
  where
    "oddity (Succ(Succ n)) = n
     | oddity Zero = Zero"
  
  partial_function (tailrec) oddity :: "nat =&gt; nat"
  where
    "oddity n =
     (if n = Zero then Zero
      else if (n &gt;= 2)
        then do { m ← oddity (n-2); m })"
  </code></pre>
  
  <p>None of them worked. I guess my attempts have conceptual and syntactic problems, what are these?</p>