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 >>