*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, Makarius <makarius at sketis.net>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] RC5: Syntactic class bit_operations is gone*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 12 Feb 2021 20:42:37 +0000*In-reply-to*: <76255ab4-6650-ff80-f765-53eebc7cf60b@informatik.tu-muenchen.de>*References*: <710bf85d-0628-a7dd-75e6-9709488313a2@sketis.net> <d4652c65e1e1a3bd23a7e775c3a26d24c8b40fe2.camel@in.tum.de> <76255ab4-6650-ff80-f765-53eebc7cf60b@informatik.tu-muenchen.de>*User-agent*: Evolution 3.36.4-0ubuntu1

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 >

**Follow-Ups**:**Re: [isabelle] RC5: Syntactic class bit_operations is gone***From:*Florian Haftmann

**References**:**[isabelle] Isabelle2021-RC5 available for applications***From:*Makarius

**[isabelle] RC5: Syntactic class bit_operations is gone***From:*Peter Lammich

**Re: [isabelle] RC5: Syntactic class bit_operations is gone***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] RC5: Syntactic class bit_operations is gone
- Next by Date: Re: [isabelle] RC5: Syntactic class bit_operations is gone
- Previous by Thread: Re: [isabelle] RC5: Syntactic class bit_operations is gone
- Next by Thread: Re: [isabelle] RC5: Syntactic class bit_operations is gone
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list