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