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



@lukas: thanks for the hint.
@rene: sorry, I confused two things (map and mapM) so, Rene's suggestion
is orthogonal to what I said and indeed a useful lemma missing from
Option.thy in HOL.

cheers

chris

On 02/17/2012 08:32 PM, Lukas Bulwahn wrote:
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








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