Re: [isabelle] partial_function

Dear Christian,

Are you aware of

(not that it contains too much information either, but it might help establish an intuition about the internal construction).

Also in IsaFoR we use partial_functions sometimes (mostly for the option monad, which is already set up). See, e.g.,

for setting up a new datatype.

hope this helps


On 02/24/2013 06:10 AM, Christian Urban wrote:

Dear All,

I am trying to figure out whether a function I want to
define can be defined with the partial_function command
(fun and function will definitely not work).

Is there some documentation about how this command
works and which functions it can and cannot define?
There are two nice examples in Fundefs.thy (see below)
and another one in RBT_Impl.thy. I also found somewhere
that I can define a minimisation operation, which is
related to the function I want to define.

The problem is that from these handful of examples it is
very hard to find out what is going on, and when I try
to define the function I am interested in then I am asked
to discharge proof obligations of the form

  mono_option (%f. Some (least (%r. f (recf, r # ba) = Some 0)))

and I have no idea when such proof-obligations are provable
and when not.

Anybody knows more about partial_function and documentation?

Thanks a lot and best wishes,

partial_function (option)
   collatz :: "nat => nat list option"
   "collatz n =
   (if n <= 1 then Some [n]
    else if even n
      then do { ns <- collatz (n div 2); Some (n # ns) }
      else do { ns <- collatz (3 * n + 1);  Some (n # ns)})"

partial_function (tailrec)
   fixpoint :: "('a => 'a) => 'a => 'a"
   "fixpoint f x = (if f x = x then x else fixpoint f (f x))"

partial_function (tailrec)
   findzero :: "(nat => nat) => nat => nat"
   "findzero f n = (if f n = 0 then n else findzero f (Suc n))"

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.