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

René Thiemann rene.thiemann at uibk.ac.at
Fri Feb 17 11:59:05 CET 2012

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)


More information about the isabelle-dev mailing list