Re: [isabelle] recdef woes


The following congruence rule for bounded universial quantification solves your

lemma ball_cong[recdef_cong]: 
  "[| M = M'; !!x. x : M ==> P x = P' x |]
  ==> (ALL x: M. P x) = (ALL x: M'. P' x)"
  by auto

After this, recdef behaves nicely.

If you were using "list_all" instead, a similar rule for list_all would be
needed. The reason that it works out of the box when you use "map" is simply
that a congruence rule is included by default.

Hope this helps


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