*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] partial_function*From*: Christian Urban <christian.urban at kcl.ac.uk>*Date*: Sat, 9 Mar 2013 16:14:42 +0000*Cc*: Christian Urban <christian.urban at kcl.ac.uk>, Christian Sternagel <c.sternagel at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*References*: <1361442177.59055.YahooMailClassic@web120601.mail.ne1.yahoo.com> <51285F1D.5010806@gmail.com> <m27glyd9dt.fsf@kcl.ac.uk> <512966F0.2070707@gmail.com> <36584C3C-3334-4D17-92CE-E09E12511852@uibk.ac.at>*Reply-to*: christian.urban at kcl.ac.uk

Dear René, dear Christian, Thanks a lot for the helpful pointers! Best wishes, Christian On Monday, February 25, 2013 at 09:55:59 (+0100), René Thiemann wrote: > 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))" > >> > >> > > > > > > --

- Previous by Date: Re: [isabelle] Recommended use of try and try0
- Next by Date: Re: [isabelle] Updating to a previous Document.Version using Isabelle/Scala
- Previous by Thread: Re: [isabelle] Easily using built-in tactics at the ML level (and/or using a method as a tactic)
- Next by Thread: Re: [isabelle] Updating to a previous Document.Version using Isabelle/Scala
- Cl-isabelle-users March 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