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



Hi Florian,

thanks for the response and pointers to the AFP word developments.


> 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" …
> 

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. 

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



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

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.


--
  Peter
> 





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