Clever Geek Handbook

How do I define a partial function in Isabelle?

I tried to define a partial function with a keyword partial_function

. This does not work. Here's the one that best reflects your intuition:

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 is it?

+3


source to share


2 answers


There are two problems with your definitions:

  • partial_function

    does not support pattern matching on the left. This needs to be emulated using the expressions case

    on the right.

  • The type constructors nat

    are Suc

    and 0

    , not Succ

    and Zero

    . That's why your case-expression generates an error that Succ

    and Zero

    are not the designers of data types, and why parital_function

    complains that Zero

    an additional variable on the right side.

Thus, the following works:



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

You can restore the simplification rules with pattern matching using the transform simp_of_case

from ~~/src/HOL/Library/Simps_Case_Conv

:

simps_of_case oddity_simps[simp]: oddity.simps

thm oddity_simps
+5


source


Some comments regarding your last example:



  • Isabelle / HOL has no if-then

    without else

    . So a syntax error. To fix this, you'll either have to provide a else

    -branch for your last one if

    , or rewrite the definition. For example.

    partial_function (tailrec) oddity :: "nat ⇒ nat"
where
  "oddity n = (
    if n = 0 then 0
    else if n ≥ 2 then do { m ← oddity (n - 2); m }
    else undefined)"

  • At this point, an "unresolved adhoc overload" message appears. Remember that do-notation is just syntactic sugar. Let's try to see what's really going on by just looking at a do block with a block

    term "do { m ← oddity (n - 2); m }"

    Since the so far unresolved overloading allows you to fix the type m

    before 'a list

    and also disable the "pretty printable" for the overload of adhoc like this

    declare [[show_variants]]
term "do { m ← oddity (n - 2); (m :: 'a list) }"

    Result

    "List.bind (oddity (n - 2)) (λm. m)"

    So, you can see that ;

    a constant is inserted instead of the semicolon you entered bind

    (the exact constant depends on the type). The type is nat

    not registered bind

    , hence the above error. While you could define some sort of "identity monad", it rather shows that do-notation doesn't make much sense here. How about the following definition?

    partial_function (tailrec) oddity :: "nat ⇒ nat"
where
  "oddity n = (
    if n = 0 then 0
    else if n ≥ 2 then oddity (n - 2)
    else undefined)"

    Update: . For completeness, let's see how we might define the aforementioned monad. First we need a bind operation, i.e. A constant that takes a monodal identity and a function that returns an identical monad and combines these arguments into a monodal identity. The first and simplest idea might be

    definition "bind_id' x f = f x"

    which is just a functional application in reverse. However, with this definition, we will later get the monotony problems we bind_id'

    need for (tailrec)

    . So we use instead

    definition "bind_id x f = (if x = undefined then undefined else f x)"

    which guarantees that bind_id x f

    undefined

    when x

    there is, and therefore is monotonic. We then register this new constant for the adhoc overload of monadic binding like so:

    adhoc_overloading
  Monad_Syntax.bind bind_id

    Now it remains to prove the monotony of bind_id

    wrt mono_tailrec

    , which remains as an exercise (just imitate what has already been done for mono_option

    in Partial_Function

    ). Then your definition using do-notation will be accepted.

  • Perhaps you don't intend oddity 1

    undefined. But since I am not sure about the purpose oddity

    , I cannot be sure about this.

+3


source






More articles:


All Articles