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



Hi Peter,

> In 2020, there used to be a purely syntactic class for bitwise
> operations: 
> 
> HOL/Word/Bits.bit_operations
> 
> This class is gone in RC5, and the closest match seems to be the class
> semiring_bit_operations in Library/Bit_Operations.thy, but this has
> axioms.
> 
> This new class binds the infix syntax for (AND), (OR), (XOR) to these
> axioms.
>
> In my application, I cannot use the semiring_bit_operations class, as I
> cannot define a mask function. However, I'd like to use the convenient
> syntax, which is now somewhat blocked.

With Isabelle2021 you will be able to mixin bundles at every logically
relevant position, so the canonical solution for re-using mixfix syntax is

bundle and_or_xor_syntax
begin

no_notation "and" …
notation "and" …

…

end

Beyond that, what is your particular instance such that a mask operation
would not be definable?

> I thought it would be standard to define syntactic type classes for
> infix syntax first, and then add the axioms.

No.  In ancient times this was the only possibility, and hence there are
many syntactic type classes in HOL like plus, minus, times etc.

Sometimes they are necessary to accomplish a particular hierarchy, AFAIR
for gcd, lcm etc.

Syntax type classes typically forces many manual type constraints.  You
can see the traces e.g. in the upcoming AFP, entry Word_Lib, theory
Word_Syntax.thy

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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