[isabelle-dev] Word Libraries

[Florian Haftmann]

A clarifying remark:

> An observation: Normalization rules for words typically work by
> rewriting to int. This approach is historic – normalization could be
> achieved by more elementary rewriting in most cases. At least this seems
> to be the cause for the illusion of implicit normalization of word numerals:
> 
> unbundle bit_operations_syntax
> 
> lemma
>   ‹w = 1705› for w :: ‹8 word›
>   apply simp \<comment> ‹no normalization›
>   oops
> 
> lemma
>   ‹w = 1705 AND 255› for w :: ‹8 word›
>   apply simp \<comment> ‹normalizes due to rewriting to int›
>   oops
> 

This does only refer to Word.thy proper.

In Word_Lib, there is theory Norm_Words.thy which does a normalization
of word numerals except ‹- 1›; according to its examples, it works as
advertized.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211010/daa43150/attachment.sig>