Re: [isabelle] partial_function



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

-- 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.