Lex Bailey (Jan 27 2023 at 14:47): Lex Bailey (Jan 27 2023 at 14:47):Hi,
as part of a larger proof for something I'm working on, I need to prove something like the following...
lemma div_pow2_le_mono:
shows "(reg::nat) ≤ n ⟶ (reg div (2^d)) ≤ (n div (2^d))"
by (simp add: div_le_mono)
This works as expected for the nat type, but I specifically want to use 8 word instead of nat (this is modelling a right bit shift on a byte register)
so I am trying to prove something like the following, which uses drop_bit on word types:
lemma
shows "(reg :: 8 word) ≤ a ⟶ (drop_bit k reg) ≤ a div 2^k"
apply transfer
apply (simp add: div_le_mono div_pow2_le_mono)
...
I had hoped that with transfer I would be able to prove this for words in much the same way as with nats, but it appears not to work.
Am I missing something? Is there an easy way to do this? If not then how best to prove this lemma?
Thanks :)
Christian Pardillo Laursen (Jan 27 2023 at 18:01):lemma "(reg :: 8 word) ≤ a ⟶ (drop_bit k reg) ≤ a div 2^k"
by (simp add: drop_bit_eq_div word_le_nat_alt unat_div_distrib div_le_mono)
Unfolding the definition of leq for words lets you prove the same fact on naturals
Lex Bailey (Jan 29 2023 at 02:52):ah! awesome, thanks :)
Last updated: Apr 24 2024 at 16:18 UTC