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
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?
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 2023 at 08:19 UTC