[isabelle-dev] Some missing setup for function package in combination with Option-type
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Some missing setup for function package in combination with Option-type
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Some missing setup for function package in combination with Option-type
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
