*To*: Peter Lammich <lammich at in.tum.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*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 13 Feb 2021 10:18:45 +0100*Autocrypt*: addr=florian.haftmann at informatik.tu-muenchen.de; keydata= mDMEW4pH0BYJKwYBBAHaRw8BAQdAIIBLFhTF7RSAZredeYMftpgRJZSF5X3VVtso084X3660 PUZsb3JpYW4gSGFmdG1hbm4gPGZsb3JpYW4uaGFmdG1hbm5AaW5mb3JtYXRpay50dS1tdWVu Y2hlbi5kZT6IlgQTFggAPgIbAwULCQgHAgYVCgkICwIEFgIDAQIeAQIXgBYhBILJqbJrurlT 4Zn85KcHFyIyz6TpBQJf7KrvBQkGZIwfAAoJEKcHFyIyz6Tp/ugBAL2yRfjY1/2YxFcedOFp bRJFZ7H7SGVL0UeX9hLNOanwAP9PCZrz644aWsVleb52yi/CL0K8Q/WfXLH76xhpYGQLCrg4 BFuKR9ASCisGAQQBl1UBBQEBB0CU8ZQJlBvMpEyGnR4jpUF+HavpBguEs4uAxFQBY21SHgMB CAeIfgQYFggAJgIbDBYhBILJqbJrurlT4Zn85KcHFyIyz6TpBQJf7Kt0BQkGZIykAAoJEKcH FyIyz6TpTTYA/0ysxqOA8YYInFnDdp+ZoLM0Djahh4MUyQ3OCpz6U4/kAP9MfgQqCyGJskPe nGsCTrHdcW760UZ3KMge7vAVPw1eD7gzBFuKSn4WCSsGAQQB2kcPAQEHQNf9JkHWQaDR5cRm q0x7ltlUFok5Z8rfCtOZxVITGGyWiPUEGBYIACYCGwIWIQSCyamya7q5U+GZ/OSnBxciMs+k 6QUCX+yrdAUJBmSJ9gCBdiAEGRYIAB0WIQQ2aRv8hQWta5iN4IfgIQ1PG8W1PgUCW4pKfgAK CRDgIQ1PG8W1PnBCAQDX4Yp8i5GA7fZR8gysMIvUEqnewxPv5MVUrzjSxyNM9gEAvShATZq0 bLwrDJXiPvB+8WLvG9SXWgMLbvt8iSJ2wwwJEKcHFyIyz6TpAj4BAPFUzBamR3bW2iTA/s8r WX4sadNSMoD2Cem5PKQ07YzRAPwNdh4EF4XWcmAzHFyei2sp/KFUgNsgJQ8/iKAcDCRxCg==*In-reply-to*: <6bd205e1ac8f5344401f4ea35cadde9db15447c9.camel@in.tum.de>*References*: <710bf85d-0628-a7dd-75e6-9709488313a2@sketis.net> <d4652c65e1e1a3bd23a7e775c3a26d24c8b40fe2.camel@in.tum.de> <76255ab4-6650-ff80-f765-53eebc7cf60b@informatik.tu-muenchen.de> <6bd205e1ac8f5344401f4ea35cadde9db15447c9.camel@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0

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. Cheers, Florian

**Attachment:
signature.asc**

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

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

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

- 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