[isabelle-dev] Suc 0 necessary?

[Lawrence Paulson]

Believe it or not, last week I was doing actual Isabelle proofs and  
they were very cluttered by countless occurrences of Suc 0, Suc (Suc  
0) and Suc (Suc (Suc 0)). Abbreviating such numbers to #n would have  
been very helpful. The difference between #n and n would have to be  
clearly documented, of course.
Larry

On 23 Feb 2009, at 15:42, Tobias Nipkow wrote:

> 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