# Theory Word_Syntax

theory Word_Syntax
imports Bitwise_Signed Hex_Words Norm_Words Word_Type_Syntax
```(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
*)

section "Additional Syntax for Word Bit Operations"

theory Word_Syntax
imports
"HOL-Word.Word"
Bitwise_Signed
Hex_Words
Norm_Words
Word_Type_Syntax
begin

text ‹Additional bit and type syntax that forces word types.›

type_synonym word8 = "8 word"
type_synonym word16 = "16 word"
type_synonym word32 = "32 word"
type_synonym word64 = "64 word"

lemma len8: "len_of (x :: 8 itself) = 8" by simp
lemma len16: "len_of (x :: 16 itself) = 16" by simp
lemma len32: "len_of (x :: 32 itself) = 32" by simp
lemma len64: "len_of (x :: 64 itself) = 64" by simp

abbreviation
wordNOT  :: "'a::len word ⇒ 'a word"      ("~~ _"  71)
where
"~~ x == NOT x"

abbreviation
wordAND  :: "'a::len word ⇒ 'a word ⇒ 'a word" (infixr "&&" 64)
where
"a && b == a AND b"

abbreviation
wordOR   :: "'a::len word ⇒ 'a word ⇒ 'a word" (infixr "||"  59)
where
"a || b == a OR b"

abbreviation
wordXOR  :: "'a::len word ⇒ 'a word ⇒ 'a word" (infixr "xor" 59)
where
"a xor b == a XOR b"

(* testing for presence of word_bitwise *)
lemma "((x :: word32) >> 3) AND 7 = (x AND 56) >> 3"
by word_bitwise

(* FIXME: move to Word distribution *)
lemma bin_nth_minus_Bit0[simp]:
"0 < n ⟹ bin_nth (numeral (num.Bit0 w)) n = bin_nth (numeral w) (n - 1)"
by (cases n; simp)

lemma bin_nth_minus_Bit1[simp]:
"0 < n ⟹ bin_nth (numeral (num.Bit1 w)) n = bin_nth (numeral w) (n - 1)"
by (cases n; simp)

end
```