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



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:


On 12/08/12 01:27, Yannick Duchêne (Hibou57) wrote:
> Le Sun, 12 Aug 2012 01:09:39 +0200, Manuel Eberl <eberlm at in.tum.de> a
> écrit:
>
>> 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.
>
> 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).
>






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