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