[isabelle-dev] Some missing setup for function package in combination with Option-type
c-sterna at jaist.ac.jp
Fri Feb 17 12:13:03 CET 2012
In this respect, maybe the whole file
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.
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)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev