Re: [isabelle] code generation for saturated naturals



Florian,

On 18/08/2011, at 4:29 PM, Florian Haftmann wrote:

> One further remark: the lemmas nat_mult_min_left etc. are quite generic.
> These should go into a separate prelude section at the beginning of the
> theory, from where, after becoming part of the library, they should be
> move to appropriate theories in the HOL distribution.

OK.

> What also comes to my mind is that saturated numbers seem to be a nice
> example for complete lattices (with inf = min etc.).  Maybe you still
> want to add those instances.

I did this - see the attached. Thanks very much to sledgehammer for doing the most boring bits!

cheers
peter

Attachment: Saturated.thy
Description: Binary data

-- 
http://peteg.org/



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