Theory Word_Lib.Word_Syntax

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Additional Syntax for Word Bit Operations"

theory Word_Syntax
imports
  "HOL-Library.Word"
begin

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

context
  includes bit_operations_syntax
begin

abbreviation
  wordNOT  :: "'a::len word ⇒ 'a word"      (‹(‹open_block notation=‹prefix ~~››~~ _)› [70] 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"

end

end