Theory Guide

(*
 * Copyright Florian Haftmann
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*<*)
theory Guide
  imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64
begin

context semiring_bit_operations
begin

lemma bit_eq_iff:
  ‹a = b ⟷ (∀n. 2 ^ n ≠ 0 ⟶ bit a n ⟷ bit b n)›
  using bit_eq_iff [of a b] by (simp add: possible_bit_def)

end

notation (output)  Generic_set_bit.set_bit (‹Generic'_set'_bit.set'_bit›)

hide_const (open) Generic_set_bit.set_bit

no_notation bit  (infixl ‹!!› 100)

(*>*)
section ‹A short overview over bit operations and word types›

subsection ‹Key principles›

text ‹
  When formalizing bit operations, it is tempting to represent
  bit values as explicit lists over a binary type. This however
  is a bad idea, mainly due to the inherent ambiguities in
  representation concerning repeating leading bits.

  Hence this approach avoids such explicit lists altogether
  following an algebraic path:

    ▪ Bit values are represented by numeric types: idealized
      unbounded bit values can be represented by type \<^typ>‹int›,
      bounded bit values by quotient types over \<^typ>‹int›, aka \<^typ>‹'a word›.

    ▪ (A special case are idealized unbounded bit values ending
      in @{term [source] 0} which can be represented by type \<^typ>‹nat› but
      only support a restricted set of operations).

  The fundamental principles are developed in theory \<^theory>‹HOL.Bit_Operations›
  (which is part of \<^theory>‹Main›):

    ▪ Multiplication by \<^term>‹2 :: int› is a bit shift to the left and

    ▪ Division by \<^term>‹2 :: int› is a bit shift to the right.

    ▪ Concerning bounded bit values, iterated shifts to the left
    may result in eliminating all bits by shifting them all
    beyond the boundary.  The property \<^prop>‹(2 :: int) ^ n ≠ 0›
    represents that \<^term>‹n› is ∗‹not› beyond that boundary.

    ▪ The projection on a single bit is then @{thm [mode=iff] bit_iff_odd [where ?'a = int, no_vars]}.

    ▪ This leads to the most fundamental properties of bit values:

      ▪ Equality rule: @{thm [display, mode=iff] bit_eq_iff [where ?'a = int, no_vars]}

      ▪ Induction rule: @{thm [display, mode=iff] bit_induct [where ?'a = int, no_vars]}

    ▪ Characteristic properties @{prop [source] ‹bit (f x) n ⟷ P x n›}
      are available in fact collection \<^text>‹bit_simps›.

  On top of this, the following generic operations are provided:

    ▪ Singleton \<^term>‹n›th bit: \<^term>‹(2 :: int) ^ n›

    ▪ Bit mask upto bit \<^term>‹n›: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]}

    ▪ Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]}

    ▪ Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]}

    ▪ Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]}

    ▪ Bitwise negation: @{thm [mode=iff] bit_not_iff_eq [where ?'a = int, no_vars]}

    ▪ Bitwise conjunction: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]}

    ▪ Bitwise disjunction: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]}

    ▪ Bitwise exclusive disjunction: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]}

    ▪ Setting a single bit: @{thm set_bit_def [where ?'a = int, no_vars]}

    ▪ Unsetting a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}

    ▪ Flipping a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}

    ▪ Signed truncation, or modulus centered around \<^term>‹0::int›:
        @{thm [display] signed_take_bit_def [where ?'a = int, no_vars]}

    ▪ (Bounded) conversion from and to a list of bits:
        @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}

  Bit concatenation on \<^typ>‹int› as given by
    @{thm [display] concat_bit_def [no_vars]}
  appears quite
  technical but is the logical foundation for the quite natural bit concatenation
  on \<^typ>‹'a word› (see below).
›

subsection ‹Core word theory›

text ‹
  Proper word types are introduced in theory \<^theory>‹HOL-Library.Word›, with
  the following specific operations:

    ▪ Standard arithmetic:
        @{term ‹(+) :: 'a::len word ⇒ 'a word ⇒ 'a word›},
        @{term ‹uminus :: 'a::len word ⇒ 'a word›},
        @{term ‹(-) :: 'a::len word ⇒ 'a word ⇒ 'a word›},
        @{term ‹(*) :: 'a::len word ⇒ 'a word ⇒ 'a word›},
        @{term ‹0 :: 'a::len word›}, @{term ‹1 :: 'a::len word›}, numerals etc.

    ▪ Standard bit operations: see above.

    ▪ Conversion with unsigned interpretation of words:

        ▪ @{term [source] ‹unsigned :: 'a::len word ⇒ 'b::semiring_1›}

        ▪ Important special cases as abbreviations:

            ▪ @{term [source] ‹unat :: 'a::len word ⇒ nat›}

            ▪ @{term [source] ‹uint :: 'a::len word ⇒ int›}

            ▪ @{term [source] ‹ucast :: 'a::len word ⇒ 'b::len word›}

    ▪ Conversion with signed interpretation of words:

        ▪ @{term [source] ‹signed :: 'a::len word ⇒ 'b::ring_1›}

        ▪ Important special cases as abbreviations:

            ▪ @{term [source] ‹sint :: 'a::len word ⇒ int›}

            ▪ @{term [source] ‹scast :: 'a::len word ⇒ 'b::len word›}

    ▪ Operations with unsigned interpretation of words:

        ▪ @{thm [mode=iff] word_le_nat_alt [no_vars]}

        ▪ @{thm [mode=iff] word_less_nat_alt [no_vars]}

        ▪ @{thm unat_div_distrib [no_vars]}

        ▪ @{thm unat_drop_bit_eq [no_vars]}

        ▪ @{thm unat_mod_distrib [no_vars]}

        ▪ @{thm [mode=iff] udvd_iff_dvd [no_vars]}

    ▪ Operations with signed interpretation of words:

        ▪ @{thm [mode=iff] word_sle_eq [no_vars]}

        ▪ @{thm [mode=iff] word_sless_alt [no_vars]}

        ▪ @{thm sint_signed_drop_bit_eq [no_vars]}

    ▪ Rotation and reversal:

        ▪ @{term [source] ‹word_rotl :: nat ⇒ 'a::len word ⇒ 'a word›}

        ▪ @{term [source] ‹word_rotr :: nat ⇒ 'a::len word ⇒ 'a word›}

        ▪ @{term [source] ‹word_roti :: int ⇒ 'a::len word ⇒ 'a word›}

        ▪ @{term [source] ‹word_reverse :: 'a::len word ⇒ 'a word›}

    ▪ Concatenation: @{term [source, display] ‹word_cat :: 'a::len word ⇒ 'b::len word ⇒ 'c::len word›}

  For proofs about words the following default strategies are applicable:

    ▪ Using bit extensionality (facts \<^text>‹bit_eq_iff›, \<^text>‹bit_word_eqI›; fact
      collection \<^text>‹bit_simps›).

    ▪ Using the @{method transfer} method.
›


subsection ‹More library theories›

text ‹
  Note: currently, most theories listed here are hardly separate
  entities since they import each other in various ways.
  Always inspect them to understand what you pull in if you
  want to import one.

    ➧[Syntax]

      ➧[\<^theory>‹Word_Lib.Syntax_Bundles›]
        Bundles to provide alternative syntax for various bit operations.

      ➧[\<^theory>‹Word_Lib.Hex_Words›]
        Printing word numerals as hexadecimal numerals.

      ➧[\<^theory>‹Word_Lib.Type_Syntax›]
        Pretty type-sensitive syntax for cast operations.

      ➧[\<^theory>‹Word_Lib.Word_Syntax›]
        Specific ASCII syntax for prominent bit operations on word.

    ➧[Proof tools]

      ➧[\<^theory>‹Word_Lib.Norm_Words›]
        Rewriting word numerals to normal forms.

      ➧[\<^theory>‹Word_Lib.Bitwise›]
        Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions.

      ➧[\<^theory>‹Word_Lib.Bitwise_Signed›]
        Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions.

      ➧[\<^theory>‹Word_Lib.Word_EqI›]
        Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions.

    ➧[Operations]

      ➧[\<^theory>‹Word_Lib.Signed_Division_Word›]

        Signed division on word:

          ▪ @{term [source] ‹(sdiv) :: 'a::len word ⇒ 'a word ⇒ 'a word›}

          ▪ @{term [source] ‹(smod) :: 'a::len word ⇒ 'a word ⇒ 'a word›}

      ➧[\<^theory>‹Word_Lib.Aligned›] \

          ▪ @{thm [mode=iff] is_aligned_iff_udvd [no_vars]}

      ➧[\<^theory>‹Word_Lib.Least_significant_bit›]

        The least significant bit as an alias:
        @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]}

      ➧[\<^theory>‹Word_Lib.Most_significant_bit›]

        The most significant bit:

          ▪ @{thm [mode=iff] msb_int_def [of k]}

          ▪ @{thm [mode=iff] word_msb_sint [no_vars]}

          ▪ @{thm [mode=iff] msb_word_iff_sless_0 [no_vars]}

          ▪ @{thm [mode=iff] msb_word_iff_bit [no_vars]}

      ➧[\<^theory>‹Word_Lib.Bit_Shifts_Infix_Syntax›]

        Bit shifts decorated with infix syntax:

          ▪ @{thm Bit_Shifts_Infix_Syntax.shiftl_def [no_vars]}

          ▪ @{thm Bit_Shifts_Infix_Syntax.shiftr_def [no_vars]}

          ▪ @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]}

      ➧[\<^theory>‹Word_Lib.Next_and_Prev›] \

          ▪ @{thm word_next_unfold [no_vars]}

          ▪ @{thm word_prev_unfold [no_vars]}

      ➧[\<^theory>‹Word_Lib.Enumeration_Word›]

        More on explicit enumeration of word types.

      ➧[\<^theory>‹Word_Lib.More_Word_Operations›]

        Even more operations on word.

    ➧[Types]

      ➧[\<^theory>‹Word_Lib.Signed_Words›]

          Formal tagging of word types with a \<^text>‹signed› marker.

    ➧[Lemmas]

      ➧[\<^theory>‹Word_Lib.More_Word›]

          More lemmas on words.

      ➧[\<^theory>‹Word_Lib.Word_Lemmas›]

          More lemmas on words, covering many other theories mentioned here.

    ➧[Words of popular lengths].

      ➧[\<^theory>‹Word_Lib.Word_8›]

          for 8-bit words.

      ➧[\<^theory>‹Word_Lib.Word_16›]

          for 16-bit words.

      ➧[\<^theory>‹Word_Lib.Word_32›]

          for 32-bit words.

      ➧[\<^theory>‹Word_Lib.Word_64›]

          for 64-bit words. This theory is not part of  \<^text>‹Word_Lib_Sumo›, because it shadows
          names from \<^theory>‹Word_Lib.Word_32›. They can be used together, but then will have
          to use qualified names in applications.

      ➧[\<^theory>‹Word_Lib.Machine_Word_32› and \<^theory>‹Word_Lib.Machine_Word_64›]

          provide lemmas for 32-bit words and 64-bit words under the same name,
          which can help to organize applications relying on some form
          of genericity.
›


subsection ‹More library sessions›

text ‹
  ➧[\<^text>‹Native_Word›] Makes machine words and machine arithmetic available for code generation.
  It provides a common abstraction that hides the differences between the different target languages.
  The code generator maps these operations to the APIs of the target languages.
›

subsection ‹Legacy theories›

text ‹
  The following theories contain material which has been
  factored out since it is not recommended to use it in
  new applications, mostly because matters can be expressed
  succinctly using already existing operations.

  This section gives some indication how to migrate away
  from those theories.  However theorem coverage may still
  be terse in some cases.

  ➧[\<^theory>‹Word_Lib.Word_Lib_Sumo›]

    An entry point importing any relevant theory in that session.  Intended
    for backward compatibility: start importing this theory when
    migrating applications to Isabelle2021, and later sort out
    what you really need. You may need to include
   \<^theory>‹Word_Lib.Word_64› separately.

  ➧[\<^theory>‹Word_Lib.Generic_set_bit›]

    Kind of an alias: @{thm set_bit_eq [no_vars]}

  ➧[\<^theory>‹Word_Lib.Typedef_Morphisms›]

    A low-level extension to HOL typedef providing
    conversions along type morphisms.  The @{method transfer} method
    seems to be sufficient for most applications though.

  ➧[\<^theory>‹Word_Lib.Bit_Comprehension›]

    Comprehension syntax for bit values over predicates
    \<^typ>‹nat ⇒ bool›, for \<^typ>‹'a::len word›; straightforward
    alternatives exist.

  ➧[\<^theory>‹Word_Lib.Bit_Comprehension_Int›]

    Comprehension syntax for bit values over predicates
    \<^typ>‹nat ⇒ bool›, for \<^typ>‹int›; inherently non-computational.

  ➧[\<^theory>‹Word_Lib.Reversed_Bit_Lists›]

    Representation of bit values as explicit list in
    ∗‹reversed› order.

    This should rarely be necessary: the \<^const>‹bit› projection
    should be sufficient in most cases.  In case explicit lists
    are needed, existing operations can be used:

    @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}

  ➧[\<^theory>‹Word_Lib.Many_More›]

    Collection of operations and theorems which are kept for backward
    compatibility and not used in other theories in session \<^text>‹Word_Lib›.
    They are used in applications of \<^text>‹Word_Lib›, but should be migrated to there.
›

section ‹Changelog›

text ‹
  ➧[Changes since AFP 2022] ~

    ▪ Theory \<^text>‹Word_Lib.Ancient_Numeral› has been removed from session.

    ▪ Bit comprehension syntax for \<^typ>‹int› moved to separate theory
      \<^theory>‹Word_Lib.Bit_Comprehension_Int›.

  ➧[Changes since AFP 2021] ~

    ▪ Theory \<^text>‹Word_Lib.Ancient_Numeral› is not part of \<^theory>‹Word_Lib.Word_Lib_Sumo›
      any longer.

    ▪ Infix syntax for \<^term>‹(AND)›, \<^term>‹(OR)›, \<^term>‹(XOR)› organized in
      syntax bundle \<^bundle>‹bit_operations_syntax›.

    ▪ Abbreviation \<^abbrev>‹max_word› moved from distribution into theory
      \<^theory>‹Word_Lib.Legacy_Aliases›.

    ▪ Operation \<^const>‹test_bit› replaced by input abbreviation \<^abbrev>‹test_bit›.

    ▪ Abbreviations \<^abbrev>‹bin_nth›, \<^abbrev>‹bin_last›, \<^abbrev>‹bin_rest›,
      \<^abbrev>‹bintrunc›, \<^abbrev>‹sbintrunc›, \<^abbrev>‹norm_sint›,
      \<^abbrev>‹bin_cat› moved into theory \<^theory>‹Word_Lib.Legacy_Aliases›.

    ▪ Operations \<^abbrev>‹bshiftr1›,
      \<^abbrev>‹setBit›, \<^abbrev>‹clearBit› moved from distribution into theory
      \<^theory>‹Word_Lib.Legacy_Aliases› and replaced by input abbreviations.

    ▪ Operations \<^const>‹shiftl1›, \<^const>‹shiftr1›, \<^const>‹sshiftr1›
      moved here from distribution.

    ▪ Operation \<^const>‹complement› replaced by input abbreviation \<^abbrev>‹complement›.
›

(*<*)
end
(*>*)