Email Gateway (Aug 19 2022 at 08:16): Email Gateway (Aug 19 2022 at 08:16):From: Manuel Eberl <eberlm@in.tum.de>
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?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 08:16):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Have you tried to change the order of the import clauses? I remember I
read something in Isabelle's documentation, explaining how some imports
must always come last (which in turn may suggest some others have to come
before the last ones).
Email Gateway (Aug 19 2022 at 08:17):From: Manuel Eberl <eberlm@in.tum.de>
That doesn't do anything. Consider the following minimal example:
theory Test
imports Main "~~/src/HOL/Number_Theory/Cong"
begin
lemma "P (n::nat)"
proof (induction n)
print_cases
You can swap the two imports and the result is still the same:
cases:
zero:
let "?case" = "P 0"
plus1:
fix n_
let "?case" = "P (n_ + 1)"
assume plus1.IH: "P n_" and plus1.prems:
Email Gateway (Aug 19 2022 at 08:17):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Apr 19 2024 at 04:17 UTC