1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Additional Syntax for Word Bit Operations"
8
9theory Word_Syntax
10imports
11  "HOL-Word.More_Word"
12  WordBitwise_Signed
13  Hex_Words
14  Norm_Words
15  Word_Type_Syntax
16begin
17
18text \<open>Additional bit and type syntax that forces word types.\<close>
19
20type_synonym word8 = "8 word"
21type_synonym word16 = "16 word"
22type_synonym word32 = "32 word"
23type_synonym word64 = "64 word"
24
25lemma len8: "len_of (x :: 8 itself) = 8" by simp
26lemma len16: "len_of (x :: 16 itself) = 16" by simp
27lemma len32: "len_of (x :: 32 itself) = 32" by simp
28lemma len64: "len_of (x :: 64 itself) = 64" by simp
29
30
31abbreviation
32  wordNOT  :: "'a::len0 word \<Rightarrow> 'a word"      ("~~ _" [70] 71)
33where
34  "~~ x == NOT x"
35
36abbreviation
37  wordAND  :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infixr "&&" 64)
38where
39  "a && b == a AND b"
40
41abbreviation
42  wordOR   :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infixr "||"  59)
43where
44  "a || b == a OR b"
45
46abbreviation
47  wordXOR  :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infixr "xor" 59)
48where
49  "a xor b == a XOR b"
50
51(* testing for presence of word_bitwise *)
52lemma "((x :: word32) >> 3) AND 7 = (x AND 56) >> 3"
53  by word_bitwise
54
55(* FIXME: move to Word distribution *)
56lemma bin_nth_minus_Bit0[simp]:
57  "0 < n \<Longrightarrow> bin_nth (numeral (num.Bit0 w)) n = bin_nth (numeral w) (n - 1)"
58  by (cases n; simp)
59
60lemma bin_nth_minus_Bit1[simp]:
61  "0 < n \<Longrightarrow> bin_nth (numeral (num.Bit1 w)) n = bin_nth (numeral w) (n - 1)"
62  by (cases n; simp)
63
64end
65