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

isabelle-2021 asmrefine: make 64 bit clean 

The previous proof of unat_word32_less_2p_word_bits worked only for
word_bits = 32.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-09-24 08:37:51 +10:00 committed by Gerwin Klein
parent 492c236121
commit e3f50549c6
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
tools/asmrefine/CommonOpsLemmas.thy
View File

@ -38,8 +38,9 @@ lemma is_up_u32_word_size: "is_up UCAST(32 \<rightarrow> machine_word_len)"
lemma is_up_i32_word_size: "is_up UCAST(32 signed \<rightarrow> machine_word_len)"
by (clarsimp simp add: is_up_def source_size target_size)
(* This proof is a bit convoluted so that it happens to work with word_bits = 32 and 64 *)
lemma unat_word32_less_2p_word_bits: "unat (x :: 32 word) < 2 ^ word_bits"
by (fact unat_less_2p_word_bits)
unfolding word_bits_def by (rule upcast_unat_less_2p_length, rule is_up_u32_word_size)
lemma unat_sword32_less_2p_word_bits: "unat (x :: 32 signed word) < 2 ^ word_bits"
by (rule upcast_unat_less_2p_length[OF is_up_i32_word_size, simplified word_bits_def[symmetric]])