lib: add some word lemmas about sless, word_bits
This commit is contained in:
parent
e5ecf10b14
commit
df9c791a3f
|
@ -3769,6 +3769,11 @@ lemma zero_sle_ucast_up:
|
||||||
apply arith
|
apply arith
|
||||||
done
|
done
|
||||||
|
|
||||||
|
lemma word_le_ucast_sless:
|
||||||
|
"\<lbrakk> x \<le> y; y \<noteq> -1; LENGTH('a) < LENGTH('b) \<rbrakk> \<Longrightarrow>
|
||||||
|
UCAST (('a :: len) \<rightarrow> ('b :: len) signed) x <s ucast (y + 1)"
|
||||||
|
by (clarsimp simp: word_le_make_less word_sless_alt sint_ucast_eq_uint is_down word_less_def)
|
||||||
|
|
||||||
lemma msb_ucast_eq:
|
lemma msb_ucast_eq:
|
||||||
"len_of TYPE('a) = len_of TYPE('b) \<Longrightarrow>
|
"len_of TYPE('a) = len_of TYPE('b) \<Longrightarrow>
|
||||||
msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)"
|
msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)"
|
||||||
|
|
|
@ -84,6 +84,12 @@ lemma unat_less_word_bits:
|
||||||
lemmas unat_mask_word64' = unat_mask[where 'a=64]
|
lemmas unat_mask_word64' = unat_mask[where 'a=64]
|
||||||
lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
|
lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
|
||||||
|
|
||||||
|
lemma unat_less_2p_word_bits:
|
||||||
|
"unat (x :: 64 word) < 2 ^ word_bits"
|
||||||
|
apply (simp only: word_bits_def)
|
||||||
|
apply (rule unat_lt2p)
|
||||||
|
done
|
||||||
|
|
||||||
lemma Suc_unat_mask_div:
|
lemma Suc_unat_mask_div:
|
||||||
"Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)"
|
"Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)"
|
||||||
apply (case_tac "sz < word_bits")
|
apply (case_tac "sz < word_bits")
|
||||||
|
|
Loading…
Reference in New Issue