[isabelle-dev] Some missing setup for function package in combination with Option-type

[Lukas Bulwahn]

Just two comments:

First, the discussion about this should be on the isabelle mailing list, 
not the isabelle developer's mailing list.
There has been a discussion just a few days ago that the developer's 
mailing list is limited to arbitrary repository versions and the related 
development process, including administrative things like isatest, mira etc.

Second, the AFP is a perfect place to also submit small library 
developments. The List-Index theory is such an example.
So, the Option monad could be just turned into a small AFP entry.


Lukas


On 02/17/2012 12:13 PM, Christian Sternagel wrote:
> In this respect, maybe the whole file
>
> http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/10e7033da765/IsaFoR/Option_Monad.thy 
>
>
> is of interest (which includes this cong rule already for some time). 
> If I remember correctly there was no Option.map when we wrote this. 
> Anyways, this could be (at least partly) merged into Option.thy.
>
> cheers
>
> chris
>
> On 02/17/2012 07:59 PM, René Thiemann wrote:
>> Dear all,
>>
>> recently, I stumbled upon the problem, that there is no proper 
>> fundef-cong rule for map on Option-types.
>>
>> I added it manually to our developedment, but perhaps this should be 
>> integrated in Option.thy
>>
>> lemma option_map_cong[fundef_cong]:
>> "xs = ys \<Longrightarrow>  \<lbrakk>\<And>  x. ys = Some x 
>> \<Longrightarrow>  f x = g x\<rbrakk>  \<Longrightarrow>  Option.map 
>> f xs = Option.map g ys"
>>    by (cases ys, auto)
>>
>> Cheers,
>> René
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>