From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
is it possible to see the details of the proof of
Suc n ≠ 0
?
This is an automatic proof so the proof script is not easily available I guess.
From: Larry Paulson <lp15@cam.ac.uk>
This is virtually an atomic statement, so in effect you are asking for the details of how datatypes are represented internally. This representation has always been complicated, and I think the new system is even more complicated.
Larry Paulson
From: Andrei Popescu <a.popescu@mdx.ac.uk>
Hi Gergely,
Suc n ≠ 0
Indeed, this holds "by construction." The papers
http://www.eis.mdx.ac.uk/staffpages/andreipopescu/pdf/LICS2012.pdf
http://www.eis.mdx.ac.uk/staffpages/andreipopescu/pdf/codat-impl.pdf
give details on how the construction is currently performed in Isabelle/HOL.
That fact is an instance of a general phenomenon: the structural morphism of the initial algebra (a.k.a. the constructor) is injective.
Best,
Andrei
Last updated: Mar 29 2024 at 08:18 UTC