Theory Word_Lib.Signed_Words
section "Signed Words"
theory Signed_Words
imports "HOL-Library.Word"
begin
text ‹Signed words as separate (isomorphic) word length class. Useful for tagging words in C.›
typedef ('a::len0) signed = "UNIV :: 'a set" ..
lemma card_signed [simp]: "CARD (('a::len0) signed) = CARD('a)"
unfolding type_definition.card [OF type_definition_signed]
by simp
instantiation signed :: (len0) len0
begin
definition
len_signed [simp]: "len_of (x::'a::len0 signed itself) = LENGTH('a)"
instance ..
end
instance signed :: (len) len
by (intro_classes, simp)
lemma scast_scast_id [simp]:
"scast (scast x :: ('a::len) signed word) = (x :: 'a word)"
"scast (scast y :: ('a::len) word) = (y :: 'a signed word)"
by (auto simp: is_up scast_up_scast_id)
lemma ucast_scast_id [simp]:
"ucast (scast (x :: 'a::len signed word) :: 'a word) = x"
by transfer (simp add: take_bit_signed_take_bit)
lemma scast_of_nat [simp]:
"scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)"
by transfer (simp add: take_bit_signed_take_bit)
lemma scast_ucast_id [simp]:
"scast (ucast (x :: 'a::len word) :: 'a signed word) = x"
by transfer (simp add: take_bit_signed_take_bit)
lemma scast_eq_scast_id [simp]:
"((scast (a :: 'a::len signed word) :: 'a word) = scast b) = (a = b)"
by (metis ucast_scast_id)
lemma ucast_eq_ucast_id [simp]:
"((ucast (a :: 'a::len word) :: 'a signed word) = ucast b) = (a = b)"
by (metis scast_ucast_id)
lemma scast_ucast_norm [simp]:
"(ucast (a :: 'a::len word) = (b :: 'a signed word)) = (a = scast b)"
"((b :: 'a signed word) = ucast (a :: 'a::len word)) = (a = scast b)"
by (metis scast_ucast_id ucast_scast_id)+
lemma scast_2_power [simp]: "scast ((2 :: 'a::len signed word) ^ x) = ((2 :: 'a word) ^ x)"
by (rule bit_word_eqI) (auto simp add: bit_simps)
lemma ucast_nat_def':
"of_nat (unat x) = (ucast :: 'a :: len word ⇒ ('b :: len) signed word) x"
by (fact of_nat_unat)
lemma zero_sle_ucast_up:
"¬ is_down (ucast :: 'a word ⇒ 'b signed word) ⟹
(0 <=s ((ucast (b::('a::len) word)) :: ('b::len) signed word))"
by transfer (simp add: bit_simps)
lemma word_le_ucast_sless:
"⟦ x ≤ y; y ≠ -1; LENGTH('a) < LENGTH('b) ⟧ ⟹
(ucast x :: ('b :: len) signed word) <s ucast (y + 1)"
for x y :: ‹'a::len word›
apply (cases ‹LENGTH('b)›)
apply simp_all
apply transfer
apply (simp add: signed_take_bit_take_bit)
apply (metis add.commute mask_eq_exp_minus_1 take_bit_incr_eq zle_add1_eq_le)
done
lemma zero_sle_ucast:
"(0 <=s ((ucast (b::('a::len) word)) :: ('a::len) signed word))
= (uint b < 2 ^ (LENGTH('a) - 1))"
apply transfer
apply (cases ‹LENGTH('a)›)
apply (simp_all add: take_bit_Suc_from_most bit_simps)
apply (simp_all add: bit_simps disjunctive_add)
done
lemma nth_w2p_scast:
"(bit (scast ((2::'a::len signed word) ^ n) :: 'a word) m)
⟷ (bit (((2::'a::len word) ^ n) :: 'a word) m)"
by (simp add: bit_simps)
lemma scast_nop1 [simp]:
"((scast ((of_int x)::('a::len) word))::'a signed word) = of_int x"
by transfer (simp add: take_bit_signed_take_bit)
lemma scast_nop2 [simp]:
"((scast ((of_int x)::('a::len) signed word))::'a word) = of_int x"
by transfer (simp add: take_bit_signed_take_bit)
lemmas scast_nop = scast_nop1 scast_nop2 scast_id
type_synonym 'a sword = "'a signed word"
end