Re: [isabelle] code generation for saturated naturals


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.


> 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!


Attachment: Saturated.thy
Description: Binary data


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