[isabelle-dev] Suc 0 necessary?

[Lawrence Paulson]

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