[isabelle] New nat induct rule in Cong.thy


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 archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.