Re: [isabelle] recdef woes

Alexander Krauss writes:
> The following congruence rule for bounded universial quantification
> solves your problem:
> 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.
I still don't understand why list_all on its own didn't work, but 
when I combined list_all with map it did work.  Anyway, thanks for the
help in finding a workaround.



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