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.

Michael.


  






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