*To*: Christian Urban <christian.urban at kcl.ac.uk>*Subject*: Re: [isabelle] partial_function*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Mon, 25 Feb 2013 09:55:59 +0100*Cc*: Christian Sternagel <c.sternagel at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <512966F0.2070707@gmail.com>*References*: <1361442177.59055.YahooMailClassic@web120601.mail.ne1.yahoo.com> <51285F1D.5010806@gmail.com> <m27glyd9dt.fsf@kcl.ac.uk> <512966F0.2070707@gmail.com>

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

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

**Re: [isabelle] partial_function***From:*Christian Sternagel

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