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
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
