Re: [isabelle] defining nat1 in isabelle




Am 15/04/2013 17:39, schrieb Leo Freitas:
> Hi,
> 
> I am new to Isabelle and its type ways of declaring / defining new types.
> In particular when extending type classes like say nat1 as an extension of nat (n > 0).

You will not become a happy person if you define your own type nat1 because
there will be zero automation for it. You will have to duplicate everything that
is there for nat already, slowly, over time. Or you constantly convert between
nat and nat1, because all the predefined functions operate on nat. I don't
recommend it.

Just for terminology: nat is a type, not a type class.

Tobias

> I couldn't find it in the sources and I wondered if someone has done this already.
> 
> Looking at Nat.thy and Orderings.thy I saw the main aspects of Nat characterisation
> but failed to properly extend my theory to cope with something like nat1.
> 
> Any help / clues is much appreciated.
> 
> Best,
> Leo
> 




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