Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Word theory and shift operations

Email Gateway (Apr 22 2025 at 03:11):

From: Alain Kägi <cl-isabelle-users@lists.cam.ac.uk>
At some point in the past, the Word theory included explicit definitions
for shift operations (e.g., shiftl1). These definitions seem to have
disappeared. Is the expectation that derivative theories use multiplication
and division by powers of 2 instead? It seemed also convenient to express
shifts with the ">>"-and-friends operators but these definitions have
disappeared as well.

Alain

Email Gateway (Apr 22 2025 at 09:44):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
It's been generalized to a type-class. Get them back like this (you'll
need the AFP for Word_Lib):

theory Scratch
imports Main "Word_Lib.Bit_Shifts_Infix_Syntax"
begin

typ "'a::semiring_bit_operations"
term "a << b"

value "(129::64 word) >> 3"
value "(5::64 word) << 3"
value "sint (((-5)::64 word) >>> 2)"

--

Peter

On 22/04/2025 05:10, Alain Kägi (via cl-isabelle-users Mailing List) wrote:

At some point in the past, the Word theory included explicit
definitions for shift operations (e.g., shiftl1). These definitions
seem to have disappeared. Is the expectation that derivative theories
use multiplication and division by powers of 2 instead? It seemed also
convenient to express shifts with the ">>"-and-friends operators but
these definitions have disappeared as well.

Alain

Email Gateway (Apr 22 2025 at 17:35):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi Alain,

note that session Word_Lib in AFP contains a small guide giving an
overview on bit and word operations.

Find that online at

https://www.isa-afp.org/browser_info/current/AFP/Word_Lib/document.pdf

Hope this helps,
Florian

Am 22.04.25 um 05:10 schrieb Alain Kägi (via cl-isabelle-users Mailing
List):

At some point in the past, the Word theory included explicit definitions
for shift operations (e.g., shiftl1). These definitions seem to have
disappeared. Is the expectation that derivative theories use
multiplication and division by powers of 2 instead? It seemed also
convenient to express shifts with the ">>"-and-friends operators but
these definitions have disappeared as well.

Alain

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: May 06 2025 at 08:28 UTC