*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] partial_function*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Sun, 24 Feb 2013 10:03:44 +0900*In-reply-to*: <m27glyd9dt.fsf@kcl.ac.uk>*References*: <1361442177.59055.YahooMailClassic@web120601.mail.ne1.yahoo.com> <51285F1D.5010806@gmail.com> <m27glyd9dt.fsf@kcl.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130219 Thunderbird/17.0.3

Dear Christian, Are you aware of http://www4.informatik.tu-muenchen.de/~krauss/mrec/mrec.pdf

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 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))"

**Follow-Ups**:**Re: [isabelle] partial_function***From:*René Thiemann

**References**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Andrei Popescu

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

**[isabelle] partial_function***From:*Christian Urban

- Previous by Date: [isabelle] partial_function
- Next by Date: [isabelle] new AFP entry: Launchbury
- Previous by Thread: [isabelle] partial_function
- Next by Thread: Re: [isabelle] partial_function
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list