[isabelle-dev] Suc 0 necessary?

[Tobias Nipkow]

I don't think it was me who argued against #n a number of years back...

Tobias

Lawrence Paulson wrote:
> 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 
>>>>