[isabelle-dev] Suc 0 necessary?

[Brian Huffman]

I'd be interested to learn more about the background of the "Suc 0"  
issue; this is the first time I've seen it discussed on the mailing  
list.

What I see as the deeper question is, why is "1 = Suc 0" declared as a  
simp rule?

There are two possible views of type nat:

1) an inductive datatype with values 0, Suc 0, Suc (Suc 0), ...
2) an abstract numeric type with values 0, 1, 2, 3, 4, 5 ...

By having "1 = Suc 0" declared [simp], it seems that users are  
required to take view 1 to a certain extent, whether they want to or  
not. It is actually difficult to use view 2 (for example,  
Library/Euclidean_Space.thy tries to use view 2; it has "simp del:  
One_nat_def" all over the place).

Doesn't it make sense to leave it to users to decide which  
representation they want? Is there really any convincing reason why "1  
= Suc 0" needs to be a simp rule?

- Brian

Quoting Tobias Nipkow <nipkow at in.tum.de>:

> This translation is not in there by default because it is bound to
> confuse novices and sometimes even experts: they see 1 in their proof
> state and 1 in their theorem and wonder why Isabelle refuses to apply
> the theorem. And eventually they realise that one of the two 1s is a Suc
> 0, whereas the other one is a genuine 1.
>
> Of course, we avoid the above frustration at the cost of Suc 0.
>
> This issue comes up again and again, and we are not happy with the
> current state either. Thanks for your input.
>
> Tobias
>
> Chris Capel schrieb:
>> translations
>>   "1" <= "Suc 0"
>>   "2" <= "Suc (Suc 0)"
>>
>> Is there a reason why the above isn't defined by default? Is it a
>> matter of preference? Context? As a translation, the above doesn't
>> interfere with simplification machinery, so I don't think including it
>> by default would do any harm. Of course, not including it would be
>> fine too. But in the latter case perhaps the statement could be
>> mentioned in documentation instead of the current apology for the
>> strangeness of seeing "Suc 0" where one would expect "1".
>>
>> The 2 translation isn't as important. It seems like I occasionally see
>> "Suc (Suc 0)", but I don't think the simplifier will ever leave it.
>>
>> Chris Capel
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>