[isabelle-dev] Suc 0 necessary?
nipkow at in.tum.de
Mon Feb 23 16:54:56 CET 2009
>> This is exactly the point: recursive functions defined by pattern
>> matching expect Suc. They tend to dominate the scene in CS-oriented
>> applications. Hence Suc 0 is made the default. However, for math
>> applications this tends to be inconvenient, esp in connection with
>> abstract algebra involving 1.
> I never understood this argument completely. This solves the issue for
> 1, but not for e.g. 2 , 3, 4 etc, where we must add nat_number or do
> something else if that is too dangerous. Isn't that so?
This is based on the empirical fact that expanding 1 to Suc 0 is a good
idea because many recursive functions should be evaluated on 1. But
beyond 1, it is becomes questionable: think of what happens if you have
(a+b)^n - it is best left alone, even if n is a numeral, unless the user
believes it should be expanded.
More information about the isabelle-dev