Re: [isabelle] New nat induct rule in Cong.thy



Am 12/08/2012 01:09, schrieb Manuel Eberl:
> Hallo,
> 
> I noticed some strange behaviour with induction over nat before: instead
> of the usual 0 and Suc, the induction cases when doing induction over a
> nat were suddenly called zero and plus1 in my code, and they didn't have
> "P (Suc n)" in the induction step anymore, but "P (n + 1)".
> 
> I discovered that the problem occurs only when I import Cong.thy and
> that Cong.thy declares an alternative induction rule for nat with these
> exact case names.
> 
> Is this intended behaviour? I doubt many people usually give the
> explicit induction rule they want to use when doing induction over nat
> (nat_induct, I think), so if they then include Cong.thy or some theory
> that depends on it (like Binomial.thy), this will break all the Isar
> induction proofs over nat, does it not?

This is the intended behaviour. Jeremy Avigad, who developed the number theory
library, intended to minimize Suc in favour of +1. Now if you include (parts of)
a library, you inherit such design decisions, just like you inherit all simp
rules and all syntax. Making this more modular is a long term goal.

Tobias

> Cheers,
> Manuel
> 





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