secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

word_lib: add toEnum_unat_le 

Relates toEnum (unat x) with ucast.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2025-07-01 12:24:21 +10:00
parent aebe8c6b20
commit e8a219ffc9
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
lib/Word_Lib/Word_Lemmas_Internal.thy
View File

@ -1047,4 +1047,14 @@ lemma ucast_and_mask_source:
UCAST('a \<rightarrow> 'b::len) w && mask n = ucast w && mask LENGTH('a)" for w::"'a::len word"
by word_eqI (fastforce dest: test_bit_lenD)
lemma toEnum_unat_le:
"x \<le> ucast y \<Longrightarrow> toEnum (unat x) \<le> y" for x::"'a::len word" and y::"'b::len word"
apply (subgoal_tac "unat y < 2^LENGTH('b)")
apply (subgoal_tac "unat x < 2^LENGTH('b)")
apply (simp add: le_ucast_ucast_le)
apply (fastforce simp: word_le_nat_alt unat_ucast
elim!: order_trans order_le_less_trans[rotated])
apply simp
done
end