search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

WORD_SIMPLE_SUBWORD_CONV and related lemmas #117

Closed jargh closed 1 month ago

jargh commented 1 month ago

This adds 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)