equal
deleted
inserted
replaced
71 |
71 |
72 instance .. |
72 instance .. |
73 |
73 |
74 end |
74 end |
75 |
75 |
|
76 lemma msb_word_iff_bit: |
|
77 \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - Suc 0)\<close> |
|
78 for w :: \<open>'a::len word\<close> |
|
79 by (simp add: msb_word_def bin_sign_def bit_uint_iff) |
|
80 |
76 lemma word_msb_def: |
81 lemma word_msb_def: |
77 "msb a \<longleftrightarrow> bin_sign (sint a) = - 1" |
82 "msb a \<longleftrightarrow> bin_sign (sint a) = - 1" |
78 by (simp add: msb_word_def sint_uint) |
83 by (simp add: msb_word_def sint_uint) |
79 |
84 |
80 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0" |
85 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0" |
81 by (simp add: msb_word_eq bit_last_iff) |
86 by (simp add: msb_word_eq bit_last_iff) |
|
87 |
|
88 lemma msb_word_iff_sless_0: |
|
89 \<open>msb w \<longleftrightarrow> w <s 0\<close> |
|
90 by (simp add: word_msb_sint word_sless_alt) |
82 |
91 |
83 lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)" |
92 lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)" |
84 by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem) |
93 by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem) |
85 |
94 |
86 lemma word_msb_numeral [simp]: |
95 lemma word_msb_numeral [simp]: |