adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Word_Lib: simplify numeral + Suc 0 expressions 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-09-23 14:32:18 +10:00 committed by Gerwin Klein
parent a41eee7154
commit 414eb5ce3d
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/Word_Lib/Traditional_Infix_Syntax.thy
View File

@ -237,6 +237,14 @@ lemma sshiftr_numeral [simp]:
apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps)
done
lemma sshiftr_numeral_Suc_0 [simp]:
\<open>(numeral k >>> Suc 0 :: 'a::len word) =
word_of_int (drop_bit (Suc 0) (signed_take_bit (LENGTH('a) - 1) (numeral k)))\<close>
apply (rule word_eqI)
apply (cases \<open>LENGTH('a)\<close>)
apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps)
by (metis dual_order.antisym le_Suc_eq)
setup \<open>
Context.theory_map (fold SMT_Word.add_word_shift' [
(\<^term>\<open>shiftl :: 'a::len word \<Rightarrow> _\<close>, "bvshl"),
@ -347,6 +355,10 @@ lemma shiftl_numeral [simp]:
\<open>numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)\<close>
by (fact shiftl_word_eq)
lemma shiftl_numeral_Suc_0 [simp]:
\<open>numeral k << Suc 0 = (numeral (k * num.Bit0 num.One) :: 'a::len word)\<close>
by (subst shiftl_word_eq) simp
lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
for x :: "'a::len word"
apply transfer