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 :)
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
ah! awesome, thanks :)
Last updated: Dec 07 2024 at 16:22 UTC