Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] tracing automatic datatype theorems


view this post on Zulip Email Gateway (Aug 22 2022 at 11:45):

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.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:45):

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

view this post on Zulip Email Gateway (Aug 22 2022 at 11:45):

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