Re: [isabelle] partial_function



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.