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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
