1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Signed Words"
8
9theory Signed_Words
10imports "HOL-Word.Word"
11begin
12
13text \<open>Signed words as separate (isomorphic) word length class. Useful for tagging words in C.\<close>
14
15typedef ('a::len0) signed = "UNIV :: 'a set" ..
16
17lemma card_signed [simp]: "CARD (('a::len0) signed) = CARD('a)"
18  unfolding type_definition.card [OF type_definition_signed]
19  by simp
20
21instantiation signed :: (len0) len0
22begin
23
24definition
25  len_signed [simp]: "len_of (x::'a::len0 signed itself) = LENGTH('a)"
26
27instance ..
28
29end
30
31instance signed :: (len) len
32  by (intro_classes, simp)
33
34type_synonym 'a sword = "'a signed word"
35type_synonym  sword8 =  "8 sword"
36type_synonym sword16 = "16 sword"
37type_synonym sword32 = "32 sword"
38type_synonym sword64 = "64 sword"
39
40end
41