Re: [isabelle] tracing automatic datatype theorems

Hi Gergely, 

>   Suc n ≠ 0

Indeed, this holds "by construction."  The papers

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. 

From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of Larry Paulson [lp15 at]
Sent: Friday, October 16, 2015 5:13 PM
To: Buday Gergely
Cc: cl-isabelle-users at
Subject: Re: [isabelle] tracing automatic datatype theorems

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

> On 16 Oct 2015, at 16:25, Buday Gergely <gbuday at> wrote:
> 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.
> - Gergely


Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.

If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.