word_lib+crefine: move lemmas to Word_Lib #736
Conversation
lsf37
commented
Mar 16, 2024
lsf37
commented
- move AARCH64 word lemmas to the holding area in Word_Lib
- generalise word_ctz_upcast_id and provide word_ctz_upcast_id_32_64
lsf37
force-pushed
the
aarch64-word-move
branch
from
23c1364
to
f7989a1
Compare
lsf37
force-pushed
the
aarch64-word-move
branch
2 times, most recently
from
b39ea74
to
fc470c2
Compare
| by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq) | ||
|
|
||
| lemma word_ctz_upcast_id_32_64: | ||
| "x \<noteq> 0 \<Longrightarrow> word_ctz (UCAST(32 \<rightarrow> 64) x) = word_ctz x" |
There was a problem hiding this comment.
there's an argument to be made that this is true of any upcast
There was a problem hiding this comment.
That's why I made word_ctz_upcast_id and use it here to prove this one :-). Just wanted to preserve the behaviour the existing proof expects and remove the additional is_up condition the generic one introduces.
| @@ -1480,19 +1480,6 @@ lemma multiple_add_less_nat: | |||
| apply simp | |||
| done | |||
|
|
|||
| (* FIXME AARCH64 move to wherever we keep the from_bool/to_bool lemmas *) | |||
| lemma word_le_1_and_idem: | |||
There was a problem hiding this comment.
can you confirm that Word_Lemmas_Internal are where we keep our from_bool/to_bool lemmas?
There was a problem hiding this comment.
Word_Lemmas_Internal is the area to commit Word_Lib lemmas to that should be moved into the rest of Word_Lib at the next sync with the AFP. The from_bool/to_bool lemmas are deeper within Word_Lib, but should only move there at the sync point (otherwise we risk accidentally removing things when we sync).
There was a problem hiding this comment.
Oki, but then do you want to remove or keep the comment to move it near from/to_bool?
There was a problem hiding this comment.
word_le_1_and_idem should not actually go there, from_to_bool_le_1_idem should. word_le_1_and_idem should go where AND lemmas are. (I.e. they should all be sorted properly by content by default, so I removed that part).
lsf37
force-pushed
the
aarch64-word-move
branch
from
fc470c2
to
c9c842b
Compare
- move AARCH64 word lemmas to the holding area in Word_Lib - generalise word_ctz_upcast_id and provide word_ctz_upcast_id_32_64 Signed-off-by: Gerwin Klein <[email protected]>
lsf37
force-pushed
the
aarch64-word-move
branch
from
c9c842b
to
a5baa09
Compare
