*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] partial_function*From*: Christian Urban <christian.urban at kcl.ac.uk>*Date*: Sat, 23 Feb 2013 21:10:22 +0000*References*: <1361442177.59055.YahooMailClassic@web120601.mail.ne1.yahoo.com> <51285F1D.5010806@gmail.com>*Reply-to*: christian.urban at 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))"

**Follow-Ups**:**Re: [isabelle] partial_function***From:*Christian Sternagel

**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

- Previous by Date: [isabelle] Formal model of XML with Isabelle: a link?
- Next by Date: Re: [isabelle] partial_function
- Previous by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- 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