Re: [isabelle] RC5: Syntactic class bit_operations is gone

Hi Peter,

>> bundle and_or_xor_syntax
>> begin
>> no_notation "and" …
>> notation "and" …
> So this will effectively build a linear stack that puts the syntax in
> order. Such a bundle will only work if the conflicting theory that
> fixes the syntax in the typeclass is also loaded. 

I don't get this point.  What is the »conflicting theory«?

> Another point against bundles is, that some notations like + or * are
> overloaded many times, with different axioms holding on them.
> For example, in our separation logic for IMP/HOL, we use * as
> separating conjunction, that only fulfills the axioms when the two
> operators are, additionally, disjoint, e.g.: a##b ==> a*b=b*a

That's a different story.  I definitely don't argue to eliminate the
traditional syntactic type classes from HOL.

> My llvm formalization uses words of variable but fixed bit-length.
> I have the operation width :: ll_word => nat, that gives the width, and
> operations are only defined between words of the same width ... but
> this is deeply embedded, rather than shallowly in the type system, such
> that I can store those words in my deeply embedded LLVM value model.
> I had instantiated all the syntactic word classes, but now, I cannot
> define mask :: nat => ll_word, as it would have to 'guess' a width.
> Also, I doubt that the axioms hold unconditionally.

Note that mask is logically a plain definition in this type class (see
the Guide.thy in AFP session Word_Lib for the rationale behind).  So, it
might be sufficient for a formal definition without a semantic
meaningful content.

But the main issue seems to me indeed the quasi-partiality of AND OR
XOR.  I don't see a way to make this compatible to the class specification.

So, the bundle seems the way to go for now.  Since there is some
rationale to put the most important bit operations into HOL-Main, I once
thought to organize all infix syntax on bits in bundles anyway, to not
clutter the syntactic space of HOL-Main.  If this is once accomplished
after the release, the infix syntax is completely free.


Attachment: signature.asc
Description: OpenPGP digital signature

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