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

isabelle2021-1 word_lib: make bit_simps [simp] 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-11-16 17:09:42 +11:00 committed by Gerwin Klein
parent c9f8e023f4
commit 71e78ac126
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Word_Lib/Word_Lemmas_Internal.thy
View File

@ -23,6 +23,8 @@ unbundle bit_projection_infix_syntax
lemmas shiftl_nat_def = push_bit_eq_mult[of _ a for a::nat, folded shiftl_def]
lemmas shiftr_nat_def = drop_bit_eq_div[of _ a for a::nat, folded shiftr_def]
declare bit_simps[simp]
lemma signed_ge_zero_scast_eq_ucast:
"0 <=s x \<Longrightarrow> scast x = ucast x"
by (simp add: scast_eq_ucast word_sle_msb_le)