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