Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle 2021 Word Library


view this post on Zulip Email Gateway (Mar 05 2021 at 10:00):

From: Freek Verbeek <freek@vt.edu>
Dear all,

I am trying to update some of my Isabelle 2020 theories to Isabelle 2021. I previously made use of the libraries "HOL-Word.Word” and "HOL-Word.Word_Bitwise” and see that these have been replaced with improved versions. I am now including "HOL-Library.Word”, but I cannot find some of the things previously available (or new versions of them). For example, I cannot find the signed shiftr operator >>>, functions such as to_bl and msb, or bitwise theorems such as to_bl_plus_carry.

Does anyone know where these can be found in Isabelle 2021? I am especially looking for the bitwise theorems over arithmetic, i.e., theorems similar to “twos_complement" and “to_bl_plus_carry".

Best regards,

Freek

view this post on Zulip Email Gateway (Mar 05 2021 at 10:10):

From: Peter Lammich <lammich@in.tum.de>
Hi Freek,

there is a "Word_Lib.Word_Lib_Sumo" theory, that includes everything
...

view this post on Zulip Email Gateway (Mar 05 2021 at 11:12):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Freek,

the NEWS file contains a lot of hints and detail concerning words.

The most important one is the last:

The »Word_Lib.Word_Lib_Sumo« is a practical starting point for
migrating, personally I recommend to get along without it and switch to
more selective imports.

Hope this helps,
Florian
OpenPGP_signature


Last updated: Dec 05 2021 at 23:19 UTC