From 71e78ac126a16fd3a7d9c84d08b1f6cc2f0c3b34 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 16 Nov 2021 17:09:42 +1100 Subject: [PATCH] isabelle2021-1 word_lib: make bit_simps [simp] Signed-off-by: Gerwin Klein --- lib/Word_Lib/Word_Lemmas_Internal.thy | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 3bd2bda6d..27b3cfb9c 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_Internal.thy @@ -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 \ scast x = ucast x" by (simp add: scast_eq_ucast word_sle_msb_le)