[isabelle-dev] Suc 0 necessary?

[Tobias Nipkow]

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.

The original posting by Chris Capel merely aimed at readability: "Suc 0" 
is less pleasant than "1". An alternative we discussed but never agreed 
on is to abbreviate "Suc 0" to "#1". This would merely be new surface 
syntax and not help with the algebraic 1, but it may already satisfy 
some people.

Tobias

Lawrence Paulson wrote:
> My guess is that otherwise many obvious theorems involving 1 and 
> primitive recursive functions will not be proved. We have tangled with 
> this issue many times. It would be great to just have 1, but not if that 
> requires complicated and fragile tricks.
> Larry
> 
> On 23 Feb 2009, at 14:47, Brian Huffman wrote:
> 
>> 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 
>>>
>>>
>>>
>>
>>
>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>