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

[Christian Sternagel]

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