Commits on Oct 23, 2024

1. Added several new lemmas for "simple subwords of composite word …

   expressions":
   
       WORD_SUBWORD_INSERT_INNER
       WORD_SUBWORD_INSERT_OUTER
       WORD_SUBWORD_JOIN_LOWER
       WORD_SUBWORD_JOIN_UPPER
       WORD_SUBWORD_SUBWORD
       WORD_SUBWORD_TRIVIAL
   
   as well as a new conversion WORD_SIMPLE_SUBWORD_CONV that packages
   them up into a simplifying function, e.g.
   
     # WORD_SIMPLE_SUBWORD_CONV `word_subword (x:int16) (0,16):int16`;;
     val it : thm = |- word_subword x (0,16) = x
   
     # WORD_SIMPLE_SUBWORD_CONV
      `word_subword (word_join (x:int16) (y:int16):int32) (0,16):int16`;;
     val it : thm = |- word_subword (word_join x y) (0,16) = word_subword y (0,16)
   
     # WORD_SIMPLE_SUBWORD_CONV
      `word_subword (word_subword (x:int64) (32,32):int32) (0,16):int16`;;
     val it : thm =
       |- word_subword (word_subword x (32,32)) (0,16) = word_subword x (32,16)

   

   jargh committed Oct 23, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 2cc3f86
   • Browse repository at this point

   Copy the full SHA

   2cc3f86 View commit details

   Browse the repository at this point in the history