Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] partial_function

Email Gateway (Aug 19 2022 at 10:19):

From: Christian Urban <christian.urban@kcl.ac.uk>
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,
Christian

partial_function (option)
collatz :: "nat => nat list option"
where
"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"
where
"fixpoint f x = (if f x = x then x else fixpoint f (f x))"

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

Email Gateway (Aug 19 2022 at 10:19):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Christian,

Are you aware of

http://www4.informatik.tu-muenchen.de/~krauss/mrec/mrec.pdf

(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.,

http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/76e79c503105/IsaFoR/Parser_Monad2.thy

for setting up a new datatype.

hope this helps

chris

Email Gateway (Aug 19 2022 at 10:19):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Christian,

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

http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/76e79c503105/IsaFoR/Parser_Monad2.thy
for setting up a new datatype.

you might also refer to http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/76e79c503105/IsaFoR/Xml.thy

where for several functions, the monotonicity is proven
(Both via explicit [partial_function_mono], and also once via ML-code)

Cheers,
René

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,
Christian

partial_function (option)
collatz :: "nat => nat list option"
where
"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"
where
"fixpoint f x = (if f x = x then x else fixpoint f (f x))"

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

Email Gateway (Aug 19 2022 at 10:41):

From: Christian Urban <christian.urban@kcl.ac.uk>
Dear René, dear Christian,

Thanks a lot for the helpful pointers!

Best wishes,
Christian

Last updated: Apr 26 2024 at 16:20 UTC